nmul_le — Mathlib

English

If f is a nonnegative nonarchimedean function, then for all n ∈ ℕ and a, f(n*a) ≤ f(a).

Русский

Если f — неотрицательная неархимедова функция, то для всех n ∈ ℕ и a выполняется f(n*a) ≤ f(a).

LaTeX

$$f\ (n * a) \le f(a)$$

Lean4

/-- 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)`. -/
theorem nmul_le {F α : Type*} [NonAssocSemiring α] [FunLike F α R] [ZeroHomClass F α R] [NonnegHomClass F α R] {f : F}
    (hna : IsNonarchimedean f) {n : ℕ} {a : α} : f (n * a) ≤ f a :=
  by
  rw [← nsmul_eq_mul]
  exact nsmul_le hna

Похожие утверждения