toNat_sub — Mathlib

English

toNat(m - n) = toNat(m) - toNat(n) when n ≠ ⊤.

Русский

toNat(m - n) = toNat(m) - toNat(n) при n ≠ ⊤.

LaTeX

$$$\\\\forall n \\\\in \\\\mathbb{N}_{\\\\infty}, n \\\\neq \\\\top \\\\Rightarrow \\\\forall m \\\\in \\\\mathbb{N}_{\\\\infty}, \\\\operatorname{toNat}(m - n) = \\\\operatorname{toNat}(m) - \\\\operatorname{toNat}(n)$$$

Lean4

theorem toNat_sub {n : ℕ∞} (hn : n ≠ ⊤) (m : ℕ∞) : toNat (m - n) = toNat m - toNat n :=
  by
  lift n to ℕ using hn
  induction m
  · rw [top_sub_coe, toNat_top, zero_tsub]
  · rw [← coe_sub, toNat_coe, toNat_coe, toNat_coe]

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