ofReal_natCast — Mathlib

English

For every natural n, ENNReal.ofReal n = n; i.e., the canonical embedding of naturals via real numbers agrees with the natural cast.

Русский

Для любого натурального числа n выполнено ENNReal.ofReal n = n; каноническое вложение натуральных чисел через действительные совпадает с целочисленным отображением.

LaTeX

$$$$ \operatorname{ofReal} n = n. $$$$

Lean4

@[simp, norm_cast]
theorem ofReal_natCast (n : ℕ) : ENNReal.ofReal n = n := by simp [ENNReal.ofReal]

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