nsmul_le — Mathlib

English

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

Русский

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

LaTeX

$$f\ (n a) \le f(a) \text{ for all } n\in\mathbb{N}, 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 nsmul_le {F α : Type*} [AddMonoid α] [FunLike F α R] [ZeroHomClass F α R] [NonnegHomClass F α R] {f : F}
    (hna : IsNonarchimedean f) {n : ℕ} {a : α} : f (n • a) ≤ f a := by
  induction n with
  | zero => simp
  | succ n _ =>
    rw [add_nsmul]
    apply le_trans <| hna (n • a) (1 • a)
    simpa

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