ofReal_ofNat — Mathlib

English

For any natural n with AtLeastTwo, ENNReal.ofReal ofNat(n) = ofNat(n); the real embedding agrees with the natural cast for naturals beyond 1.

Русский

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

LaTeX

$$$$ \operatorname{ofReal} (\operatorname{ofNat} n) = \operatorname{ofNat} n. $$$$

Lean4

@[simp]
theorem ofReal_ofNat (n : ℕ) [n.AtLeastTwo] : ENNReal.ofReal ofNat(n) = ofNat(n) :=
  ofReal_natCast n

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