Theorems · Theorem · order theory

IsNonarchimedean.multiset_image_add_of_nonempty

∀ {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)

Given a nonarchimedean function α → R, a function g : β → α and a nonempty multiset s : Multiset β, we can always find b : β belonging to s such that f (t.sum g) ≤ f (g b) .

Defined in

Mathlib.Algebra.Order.Ring.IsNonarchimedean

Cited by

1 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrderAddCommMonoidNonempty