English
For m,n ∈ ℕ, the ENNReal embedding preserves natural subtraction: ↑(m − n) = (m − n) in ENNReal.
Русский
Для m,n ∈ ℕ отображение в ENNReal сохраняет вычитание: ↑(m − n) = (m − n) в ℝ≥0∞.
LaTeX
$$$$ (\uparrow (m - n) : \mathbb{R}_{\ge 0}^{\infty}) = (m - n : \mathbb{R}_{\ge 0}^{\infty}). $$$$
Lean4
@[simp, norm_cast]
theorem natCast_sub (m n : ℕ) : ↑(m - n) = (m - n : ℝ≥0∞) := by
rw [← coe_natCast, Nat.cast_tsub, coe_sub, coe_natCast, coe_natCast]