enumOrd_univ — Mathlib

English

Let enumOrd be the canonical order-preserving enumeration of ordinals on a set. If the set is the entire universe Set.univ, then the enumeration coincides with the identity map.

Русский

Пусть enumOrd — каноническое перечисление ординалов на множестве. Для полного множества ординалов (Set.univ) это перечисление совпадает с тождественным отображением.

LaTeX

$$$\\mathrm{enumOrd}(\\mathrm{Set.univ}) = \\mathrm{id}$$$

Lean4

@[simp]
theorem enumOrd_univ : enumOrd Set.univ = id := by
  rw [← range_id]
  exact enumOrd_range strictMono_id

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