toENatAux_eq_nat — Mathlib

English

For any x ∈ Cardinal and n ∈ ℕ, toENatAux x = n if and only if x = n.

Русский

Для любого x ∈ Cardinal и n ∈ ℕ, toENatAux x = n тогда и только тогда, когда x = n.

LaTeX

$$$\\forall x \\in \\mathrm{Cardinal},\\ \\forall n \\in \\mathbb{N},\\ toENatAux(x) = n \\iff x = n$$$

Lean4

theorem toENatAux_eq_nat {x : Cardinal} {n : ℕ} : toENatAux x = n ↔ x = n := by
  simp only [le_antisymm_iff, toENatAux_le_nat, ← toENatAux_gc _, ofENat_nat]

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