∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] {F : Type u_2} {α : Type u_3} {β : Type u_4}
  [inst_2 : AddCommMonoid α] [inst_3 : FunLike F α R] [ZeroHomClass F α R] [NonnegHomClass F α R] [Nonempty β] {f : F},
  IsNonarchimedean ⇑f → ∀ (g : β → α) (t : Finset β), ∃ b, (t.Nonempty → b ∈ t) ∧ f (t.sum g) ≤ f (g b)