Theorems · Theorem · order theory

IsNonarchimedean.finset_image_add

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

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

Defined in

Mathlib.Algebra.Order.Ring.IsNonarchimedean

Cited by

5 results in Mathlib

Foundations

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

Assumes

SemiringLinearOrderAddCommMonoidNonempty