coe_eq_ofNat — Mathlib

English

Equivalence between equality of coe and ofNat in WithBot.

Русский

Эквивалентность между равенством связывания с коэрцией и с ofNat.

LaTeX

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

Lean4

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

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