ord_univ — Mathlib

English

The order type of the universal cardinal equals the universal ordinal: ord(univ) = Ordinal.univ.

Русский

Порядковый тип вселенной равен универсальному ординалу: ord(univ) = Ordinal.univ.

LaTeX

$$$\\operatorname{ord}(\\mathrm{univ}) = \\mathrm{Ordinal.univ}$$$

Lean4

@[simp]
theorem ord_univ : ord univ.{u, v} = Ordinal.univ.{u, v} :=
  by
  refine le_antisymm (ord_card_le _) <| le_of_forall_lt fun o h => lt_ord.2 ?_
  have := liftPrincipalSeg.mem_range_of_rel_top (by simpa only [liftPrincipalSeg_coe] using h)
  rcases this with ⟨o, h'⟩
  rw [← h', liftPrincipalSeg_coe, ← lift_card]
  apply lift_lt_univ'

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