coe_natCast — Mathlib

English

For natural numbers n, the Real-coercion of the canonical embedding of n into NNReal equals n itself.

Русский

Для натурального числа n, преобразование в Real от соответствующего элемента в NNReal равно самому n.

LaTeX

$$$(\uparrow(\uparrow n : \mathbb{R}_{\ge 0}) : \mathbb{R}) = n$$$

Lean4

@[simp, norm_cast]
protected theorem coe_natCast (n : ℕ) : (↑(↑n : ℝ≥0) : ℝ) = n :=
  map_natCast toRealHom n

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