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