ofNat_eq_coe — Mathlib

English

Equivalence: ofNat(n) equals some m in WithBot α iff m equals ofNat(n).

Русский

Эквивалентность: ofNat(n) = (m : WithBot α) ⇔ m = ofNat(n).

LaTeX

$$$$ \\forall n \\in \\mathbb{N},\\ [n.AtLeastTwo] \\forall m \\in \\alpha,\\ (\\mathrm{ofNat}(n) = (m : \\mathrm{WithBot}(\\alpha))) \\iff m = \\mathrm{ofNat}(n). $$$$

Lean4

@[simp]
theorem ofNat_eq_coe (n : ℕ) [n.AtLeastTwo] (m : α) : ofNat(n) = (m : WithBot α) ↔ ofNat(n) = m :=
  coe_eq_coe

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