Commit 2023-02-13 06:43 c9623a9c

View on Github →

feat: port SetTheory.Ordinal.Basic (#2217) Needed to add some explicit universes here and there, add some _aux simp lemmas, and reformat some funky inductions. What is unfortunate is that succ_one : succ (1 : Ordinal) = 2 is not true by rfl anymore.

Estimated changes

added theorem Cardinal.card_ord
added theorem Cardinal.gc_ord_card
added theorem Cardinal.lift_lt_univ'
added theorem Cardinal.lift_lt_univ
added theorem Cardinal.lift_ord
added theorem Cardinal.lift_univ
added theorem Cardinal.lt_ord
added theorem Cardinal.lt_univ'
added theorem Cardinal.lt_univ
added theorem Cardinal.mk_ord_out
added def Cardinal.ord
added theorem Cardinal.ord_card_le
added theorem Cardinal.ord_eq
added theorem Cardinal.ord_eq_Inf
added theorem Cardinal.ord_injective
added theorem Cardinal.ord_le
added theorem Cardinal.ord_le_ord
added theorem Cardinal.ord_le_type
added theorem Cardinal.ord_lt_ord
added theorem Cardinal.ord_mono
added theorem Cardinal.ord_nat
added theorem Cardinal.ord_one
added theorem Cardinal.ord_univ
added theorem Cardinal.ord_zero
added def Cardinal.univ
added theorem Cardinal.univ_id
added theorem Cardinal.univ_umax
added theorem Ordinal.add_succ
added theorem Ordinal.bot_eq_zero
added def Ordinal.card
added theorem Ordinal.card_add
added theorem Ordinal.card_eq_nat
added theorem Ordinal.card_eq_zero
added theorem Ordinal.card_le_card
added theorem Ordinal.card_le_nat
added theorem Ordinal.card_lt_nat
added theorem Ordinal.card_nat
added theorem Ordinal.card_omega
added theorem Ordinal.card_one
added theorem Ordinal.card_succ
added theorem Ordinal.card_type
added theorem Ordinal.card_typein
added theorem Ordinal.card_univ
added theorem Ordinal.card_zero
added def Ordinal.enum
added def Ordinal.enumIso
added theorem Ordinal.enum_inj
added theorem Ordinal.enum_le_enum'
added theorem Ordinal.enum_le_enum
added theorem Ordinal.enum_lt_enum
added theorem Ordinal.enum_type
added theorem Ordinal.enum_typein
added theorem Ordinal.enum_zero_le'
added theorem Ordinal.enum_zero_le
added theorem Ordinal.eq_zero_or_pos
added theorem Ordinal.induction
added theorem Ordinal.inductionOn
added theorem Ordinal.infₛ_empty
added theorem Ordinal.le_add_left
added theorem Ordinal.le_add_right
added theorem Ordinal.le_enum_succ
added theorem Ordinal.le_lift_iff
added theorem Ordinal.le_one_iff
added def Ordinal.lift
added theorem Ordinal.lift_card
added theorem Ordinal.lift_down'
added theorem Ordinal.lift_down
added theorem Ordinal.lift_id'
added theorem Ordinal.lift_id
added theorem Ordinal.lift_inj
added theorem Ordinal.lift_le
added theorem Ordinal.lift_lift
added theorem Ordinal.lift_lt
added theorem Ordinal.lift_omega
added theorem Ordinal.lift_one
added theorem Ordinal.lift_type_eq
added theorem Ordinal.lift_type_le
added theorem Ordinal.lift_type_lt
added theorem Ordinal.lift_umax'
added theorem Ordinal.lift_umax
added theorem Ordinal.lift_univ
added theorem Ordinal.lift_uzero
added theorem Ordinal.lift_zero
added theorem Ordinal.lt_lift_iff
added theorem Ordinal.lt_wf
added theorem Ordinal.max_eq_zero
added theorem Ordinal.max_zero_left
added theorem Ordinal.max_zero_right
added theorem Ordinal.nat_cast_succ
added theorem Ordinal.nat_le_card
added theorem Ordinal.nat_lt_card
added def Ordinal.omega
added theorem Ordinal.one_le_iff_pos
added theorem Ordinal.one_out_eq
added theorem Ordinal.relIso_enum'
added theorem Ordinal.relIso_enum
added theorem Ordinal.succ_ne_zero
added theorem Ordinal.succ_one
added theorem Ordinal.succ_pos
added theorem Ordinal.succ_zero
added def Ordinal.type
added theorem Ordinal.type_def'
added theorem Ordinal.type_def
added theorem Ordinal.type_empty
added theorem Ordinal.type_eq
added theorem Ordinal.type_fin
added theorem Ordinal.type_fintype
added theorem Ordinal.type_le_iff'
added theorem Ordinal.type_le_iff
added theorem Ordinal.type_lt
added theorem Ordinal.type_lt_iff
added theorem Ordinal.type_nat_lt
added theorem Ordinal.type_out
added theorem Ordinal.type_pEmpty
added theorem Ordinal.type_pUnit
added theorem Ordinal.type_preimage
added theorem Ordinal.type_sum_lex
added theorem Ordinal.type_uLift
added theorem Ordinal.type_uLift_aux
added theorem Ordinal.type_unit
added def Ordinal.typein
added theorem Ordinal.typein_apply
added theorem Ordinal.typein_enum
added theorem Ordinal.typein_inj
added theorem Ordinal.typein_lt_self
added theorem Ordinal.typein_lt_type
added theorem Ordinal.typein_one_out
added theorem Ordinal.typein_surj
added theorem Ordinal.typein_top
added def Ordinal.univ
added theorem Ordinal.univ_id
added theorem Ordinal.univ_umax
added def Ordinal
added theorem RelIso.ordinal_type_eq
added theorem WellOrder.eta
added structure WellOrder
added def WellOrderingRel