Commit 2026-04-07 10:49 8fd7a1a9

View on Github →

chore: move Ordinal.univ and Cardinal.univ to their own file (#37681) This ensures SetTheory/Ordinal/Basic stays under the 1500 line limit.

Estimated changes

deleted theorem Cardinal.aleph0_lt_univ
deleted theorem Cardinal.lift_lt_univ'
deleted theorem Cardinal.lift_lt_univ
deleted theorem Cardinal.lift_univ
deleted theorem Cardinal.lt_univ'
deleted theorem Cardinal.lt_univ
deleted theorem Cardinal.nat_lt_univ
deleted theorem Cardinal.ord_univ
deleted def Cardinal.univ
deleted theorem Cardinal.univ_id
deleted theorem Cardinal.univ_ne_zero
deleted theorem Cardinal.univ_pos
deleted theorem Cardinal.univ_umax
deleted theorem Ordinal.card_univ
deleted theorem Ordinal.lift_univ
deleted theorem Ordinal.type_lt_ordinal
deleted def Ordinal.univ
deleted theorem Ordinal.univ_id
deleted theorem Ordinal.univ_umax
added theorem Cardinal.lift_lt_univ'
added theorem Cardinal.lift_lt_univ
added theorem Cardinal.lift_univ
added theorem Cardinal.lt_univ'
added theorem Cardinal.lt_univ
added theorem Cardinal.nat_lt_univ
added theorem Cardinal.ord_univ
added def Cardinal.univ
added theorem Cardinal.univ_id
added theorem Cardinal.univ_ne_zero
added theorem Cardinal.univ_pos
added theorem Cardinal.univ_umax
added theorem Ordinal.card_univ
added theorem Ordinal.lift_univ
added def Ordinal.univ
added theorem Ordinal.univ_id
added theorem Ordinal.univ_umax