natCast_sub — Mathlib

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]

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