mk_natCast — Mathlib

English

The natural number embedding into NNReal coincides with the canonical numeral in NNReal.

Русский

Встраивание натурального числа в NNReal совпадает с каноническим числовым образом в NNReal.

LaTeX

$$$ (n : \\mathbb{N}) = \\text{OfNat.ofNat } n \\quad \\text{in } \\mathbb{R}_{\\ge 0}. $$$

Lean4

@[simp]
theorem mk_natCast (n : ℕ) : @Eq ℝ≥0 (⟨(n : ℝ), n.cast_nonneg⟩ : ℝ≥0) n :=
  NNReal.eq (NNReal.coe_natCast n).symm

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