Theorems · Theorem · order theory

IsNonarchimedean.nsmul_le

∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] {F : Type u_2} {α : Type u_3} [inst_2 : AddMonoid α]
  [inst_3 : FunLike F α R] [ZeroHomClass F α R] [NonnegHomClass F α R] {f : F},
  IsNonarchimedean ⇑f → ∀ {n : ℕ} {a : α}, f (n • a) ≤ f a

If f is a nonnegative nonarchimedean function α → R such that f 0 = 0, then for every n : ℕ and a : α, we have f (n • a) ≤ (f a).

Defined in

Mathlib.Algebra.Order.Ring.IsNonarchimedean

Cited by

2 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext

Assumes

SemiringLinearOrderAddMonoidFunLikeZeroHomClassNonnegHomClass