Universal ordinal and cardinal

Cardinal.univ is the cardinality of the cardinals themselves. Likewise, Ordinal.univ is the order type of the ordinals. These are related via Cardinal.univ.ord = Ordinal.univ and Ordinal.univ.card = Cardinal.univ.

The cardinal Cardinal.univ is strongly inaccessible. This reflects the fact that in ZFC, the cardinals form a proper class. See IsInaccessible.univ for a proof.

Implementation notes

We actually define Cardinal.univ as the cardinality of Ordinal, rather than that of Cardinal. This makes the basic API easier to set up. See Cardinal.mk_cardinal for a proof that Cardinal.univ = #Cardinal.

def Ordinal.univ : Ordinal.{max (u + 1) v}

The ordinal univ.{u, v} is the order type of Ordinal.{u} or Cardinal.{u}, as an element of Ordinal.{v} (when u < v).

Equations

• Ordinal.univ.{?u.2, ?u.1} = Ordinal.lift.{?u.1, ?u.2 + 1} (Ordinal.type fun (x1 x2 : Ordinal.{?u.2}) => x1 < x2)

def Cardinal.univ : Cardinal.{max (u + 1) v}

The cardinal univ.{u, v} is the cardinality of Ordinal.{u} or Cardinal.{u}, as an element of Cardinal.{v} (when u < v).

Equations

• Cardinal.univ.{?u.4, ?u.3} = Cardinal.lift.{?u.3, ?u.4 + 1} (Cardinal.mk Ordinal.{?u.4})

Universal ordinal

@[simp]

theorem Ordinal.type_lt_ordinal : (type fun (x1 x2 : Ordinal.{u}) => x1 < x2) = univ.{u, u + 1}

@[deprecated Ordinal.type_lt_ordinal (since := "2026-03-20")]

theorem Ordinal.univ_id : univ.{u, u + 1} = type fun (x1 x2 : Ordinal.{u}) => x1 < x2

@[simp]

theorem Ordinal.lift_univ : lift.{w, max (u + 1) v} univ.{u, v} = univ.{u, max v w}

theorem Ordinal.univ_umax : univ.{u, max (u + 1) v} = univ.{u, v}

def Ordinal.liftPrincipalSeg : PrincipalSeg (fun (x1 x2 : Ordinal.{u}) => x1 < x2) fun (x1 x2 : Ordinal.{max (u + 1) v}) => x1 < x2

Principal segment version of the lift operation on ordinals, embedding Ordinal.{u} in Ordinal.{v} as a principal segment when u < v.

Equations

• Ordinal.liftPrincipalSeg = { toRelEmbedding := Ordinal.liftInitialSeg.toRelEmbedding, top := Ordinal.univ.{?u.18, ?u.17}, mem_range_iff_rel' := Ordinal.liftPrincipalSeg._proof_3 }

@[simp]

theorem Ordinal.liftPrincipalSeg_coe : ⇑liftPrincipalSeg.toRelEmbedding = lift.{max (u + 1) v, u}

@[simp]

theorem Ordinal.liftPrincipalSeg_top : liftPrincipalSeg.top = univ.{u, v}

@[deprecated Ordinal.liftPrincipalSeg_top (since := "2026-03-20")]

theorem Ordinal.liftPrincipalSeg_top' : liftPrincipalSeg.top = type fun (x1 x2 : Ordinal.{u}) => x1 < x2

@[simp]

theorem Ordinal.card_univ : univ.{u, v}.card = Cardinal.univ.{u, v}

Universal cardinal

theorem Cardinal.univ_id : univ.{u, u + 1} = mk Ordinal.{u}

@[simp]

theorem Cardinal.lift_univ : lift.{w, max (u + 1) v} univ.{u, v} = univ.{u, max v w}

theorem Cardinal.univ_umax : univ.{u, max (u + 1) v} = univ.{u, v}

theorem Cardinal.lift_lt_univ (c : Cardinal.{u}) : lift.{u + 1, u} c < univ.{u, u + 1}

theorem Cardinal.lift_lt_univ' (c : Cardinal.{u}) : lift.{max (u + 1) v, u} c < univ.{u, v}

theorem Cardinal.aleph0_lt_univ : aleph0 < univ.{u, v}

theorem Cardinal.nat_lt_univ (n : ℕ) : ↑n < univ.{u, v}

theorem Cardinal.univ_pos : 0 < univ.{u, v}

theorem Cardinal.univ_ne_zero : univ.{u, v} ≠ 0

@[simp]

theorem Cardinal.ord_univ : univ.{u, v}.ord = Ordinal.univ.{u, v}

theorem Cardinal.lt_univ {c : Cardinal.{u + 1}} : c < univ.{u, u + 1} ↔ ∃ (c' : Cardinal.{u}), c = lift.{u + 1, u} c'

theorem Cardinal.lt_univ' {c : Cardinal.{max (u + 1) v}} : c < univ.{u, v} ↔ ∃ (c' : Cardinal.{u}), c = lift.{max (u + 1) v, u} c'

theorem Cardinal.IsStrongLimit.univ : Cardinal.univ.{u, v}.IsStrongLimit

theorem Cardinal.small_iff_lift_mk_lt_univ {α : Type u} : Small.{v, u} α ↔ lift.{v + 1, u} (mk α) < univ.{v, max u (v + 1)}