toNat_add — Mathlib

English

If m,n are finite ENat numbers, then toNat(m+n) = toNat(m) + toNat(n).

Русский

Если m,n конечны в ENat, то toNat(m+n) = toNat(m) + toNat(n).

LaTeX

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

Lean4

theorem toNat_add {m n : ℕ∞} (hm : m ≠ ⊤) (hn : n ≠ ⊤) : toNat (m + n) = toNat m + toNat n :=
  by
  lift m to ℕ using hm
  lift n to ℕ using hn
  rfl

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