Theorems · Theorem · order theory

IsNonarchimedean.finset_image_add_of_nonempty

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

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

Defined in

Mathlib.Algebra.Order.Ring.IsNonarchimedean

Cited by

3 results in Mathlib

Foundations

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

Assumes

LinearOrderAddCommMonoid