toNat_eq_iff_eq_coe — Mathlib

English

For m ∈ ENat and n ∈ ℕ with n ≠ 0, toNat(m) = n iff m = cast(n).

Русский

Для m ∈ ENat и n ∈ ℕ, n ≠ 0: toNat(m) = n ⇔ m = cast(n).

LaTeX

$$$\\\\forall m \\\\in \\\\mathbb{N}_{\\\\infty}, \\\\forall n \\\\in \\\\mathbb{N}, n \\\\neq 0 \\\\Rightarrow \\\\operatorname{toNat}(m) = n \\\\iff m = n^{\\\\mathrm{cast}}$$$

Lean4

@[simp]
theorem toNat_eq_iff_eq_coe (n : ℕ∞) (m : ℕ) [NeZero m] : n.toNat = m ↔ n = m :=
  by
  cases n
  · simpa using NeZero.ne' m
  · simp

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