nnnorm_intCast_le_one — Mathlib

English

For any integer z, the NNReal norm of z in R is at most 1.

Русский

Для любого целого z нормированная NNReal величина z в R не превосходит 1.

LaTeX

$$$\| z : R \|_{\!\! _+} \le 1\quad\text{for all } z \in \mathbb{Z}$$$

Lean4

theorem nnnorm_intCast_le_one (z : ℤ) : ‖(z : R)‖₊ ≤ 1 := by
  cases z <;>
    simpa only [Int.ofNat_eq_coe, Int.cast_natCast, Int.cast_negSucc, Nat.cast_one, nnnorm_neg] using
      nnnorm_natCast_le_one _ _

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