ofENat_toENat_eq_self — Mathlib

English

For all x ∈ Cardinal and n ∈ ℕ, toENat x = n iff x = n.

Русский

Для всех x ∈ Cardinal и n ∈ ℕ, toENat x = n тогда и только тогда, когда x = n.

LaTeX

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

Lean4

@[simp]
theorem ofENat_toENat_eq_self {a : Cardinal} : toENat a = a ↔ a ≤ ℵ₀ :=
  by
  rw [eq_comm, ← enat_gc.exists_eq_l]
  simpa only [mem_range, eq_comm] using Set.ext_iff.1 range_ofENat a

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