toENat_eq_ofNat — Mathlib

English

For any a with n ≥ 2, toENat a = ofNat(n) iff a = OfNat.ofNat(n).

Русский

Для любого a с n ≥ 2, toENat a = ofNat(n) тогда и только тогда, когда a = OfNat.ofNat(n).

LaTeX

$$$\\forall a \\in \\mathrm{Cardinal},\\ \\forall n \\in \\mathbb{N},\\ [n.\\AtLeastTwo] \\Rightarrow\\ toENat(a) = \\operatorname{ofNat}(n) \\iff a = \\operatorname{OfNat}.ofNat(n)$$$

Lean4

@[simp]
theorem toENat_eq_ofNat {a : Cardinal} {n : ℕ} [n.AtLeastTwo] : toENat a = ofNat(n) ↔ a = OfNat.ofNat n :=
  toENat_eq_nat

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