nnnorm_natCast_le_one — Mathlib

English

For every natural number n, the NNReal norm of its image in R is at most 1.

Русский

Для каждого натурального числа n нормированная NNReal величина образа n в R не превосходит 1.

LaTeX

$$$\| (n : R) \|_{\!\! _+} \le 1\quad\text{for all } n \in \mathbb{N}$$$

Lean4

theorem nnnorm_natCast_le_one (n : ℕ) : ‖(n : R)‖₊ ≤ 1 := by
  induction n with
  | zero => simp only [Nat.cast_zero, nnnorm_zero, zero_le]
  | succ n hn =>
    simpa only [Nat.cast_add, Nat.cast_one, hn, max_eq_right] using nnnorm_add_one_le_max_nnnorm_one (n : R)

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