∀ {R : Type u_1} [inst : LinearOrder R] {α : Type u_2} {β : Type u_3} [inst_1 : AddCommMonoid α] [Nonempty β]
  {f : α → R}, IsNonarchimedean f → ∀ (g : β → α) {t : Finset β}, t.Nonempty → ∃ b ∈ t, f (t.sum g) ≤ f (g b)