Ordinal

📁 Source: Mathlib/SetTheory/Cardinal/Ordinal.lean

Statistics

Metric	Count
Definitions	0
Theorems mk_biUnion_le_of_le, mk_biUnion_le_of_le_lift, mk_iUnion_Ordinal_le_of_le, mk_iUnion_Ordinal_lift_le_of_le, principal_add, principal_mul, principal_opow, card_iSup_Iio_le_card_mul_iSup, card_iSup_Iio_le_sum_card, card_iSup_le_sum_card, card_omega0_opow, card_opow_eq_of_omega0_le_left, card_opow_eq_of_omega0_le_right, card_opow_le, card_opow_le_of_omega0_le_left, card_opow_le_of_omega0_le_right, card_opow_omega0, lift_card_iSup_le_sum_card, principal_add_omega, principal_add_ord, principal_mul_omega, principal_mul_ord, principal_opow_omega, principal_opow_ord	24
Total	24

Cardinal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_biUnion_le_of_le 📖	mathematical	Cardinal instLE Ordinal.card aleph0 Set.Elem	Set.iUnion Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder	—	mk_biUnion_le_of_le_lift lift_le
mk_biUnion_le_of_le_lift 📖	mathematical	Cardinal instLE lift Ordinal.card aleph0 Set.Elem	Set.iUnion Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder	—	Set.iUnion_congr_Prop Set.biUnion_eq_iUnion Function.Surjective.range_comp OrderIso.surjective lift_le LE.le.trans_eq LE.le.trans mk_iUnion_le_lift mk_toType mul_le_mul' CanonicallyOrderedAdd.toMulLeftMono canonicallyOrderedAdd covariant_swap_mul_of_covariant_mul ciSup_le' Subtype.prop mul_eq_self aleph0_le_lift
mk_iUnion_Ordinal_le_of_le 📖	mathematical	Cardinal instLE Ordinal.card aleph0 Set.Elem	Set.iUnion Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder	—	mk_biUnion_le_of_le
mk_iUnion_Ordinal_lift_le_of_le 📖	mathematical	Cardinal instLE lift Ordinal.card aleph0 Set.Elem	Set.iUnion Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder	—	mk_biUnion_le_of_le_lift

Ordinal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_iSup_Iio_le_card_mul_iSup 📖	mathematical	—	Cardinal Cardinal.instLE card iSup Ordinal Set.Elem Set.Iio PartialOrder.toPreorder partialOrder ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot Cardinal.instMul Cardinal.lift Cardinal.instConditionallyCompleteLinearOrderBot	—	LE.le.trans card_iSup_Iio_le_sum_card Cardinal.mk_toType Equiv.iSup_comp Cardinal.sum_le_lift_mk_mul_iSup
card_iSup_Iio_le_sum_card 📖	mathematical	—	Cardinal Cardinal.instLE card iSup Ordinal Set.Elem Set.Iio PartialOrder.toPreorder partialOrder ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot Cardinal.sum ToType ToType.toOrd	—	Equiv.iSup_comp card_iSup_le_sum_card
card_iSup_le_sum_card 📖	mathematical	—	Cardinal Cardinal.instLE card iSup Ordinal ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot Cardinal.sum	—	lift_card_iSup_le_sum_card UnivLE.small univLE_of_max UnivLE.self Cardinal.lift_id'
card_omega0_opow 📖	mathematical	—	card Ordinal instPow omega0 Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.aleph0	—	card_opow_eq_of_omega0_le_left le_rfl Ne.bot_lt card_omega0
card_opow_eq_of_omega0_le_left 📖	mathematical	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder omega0 Preorder.toLT zero	card instPow Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot	—	LE.le.antisymm card_opow_le_of_omega0_le_left max_le card_le_card left_le_opow right_le_opow LT.lt.trans_le one_lt_omega0
card_opow_eq_of_omega0_le_right 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder partialOrder one Preorder.toLE omega0	card instPow Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot	—	LE.le.antisymm card_opow_le_of_omega0_le_right max_le card_le_card left_le_opow LT.lt.trans_le omega0_pos right_le_opow
card_opow_le 📖	mathematical	—	Cardinal Cardinal.instLE card Ordinal instPow SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.aleph0	—	eq_nat_or_omega0_le opow_natCast natCast_pow card_nat le_max_of_le_left Cardinal.natCast_le_aleph0 LE.le.trans card_opow_le_of_omega0_le_right le_max_right card_opow_le_of_omega0_le_left
card_opow_le_of_omega0_le_left 📖	mathematical	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder omega0	Cardinal Cardinal.instLE card instPow SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot	—	opow_zero card_one card_zero sup_of_le_left Cardinal.canonicallyOrderedAdd LE.le.trans LT.lt.le one_lt_omega0 opow_succ card_mul card_succ Cardinal.mul_eq_max_of_aleph0_le_right card_eq_zero opow_eq_zero LT.lt.not_ge omega0_pos aleph0_le_card max_comm le_imp_le_of_le_of_le sup_le_sup le_refl max_assoc max_self le_self_add Order.IsNormal.apply_of_isSuccLimit isNormal_opow LT.lt.trans_le card_iSup_Iio_le_card_mul_iSup Cardinal.lift_id bot_eq_zero' canonicallyOrderedAdd Order.IsSuccLimit.ne_bot le_ciSup_of_le Cardinal.bddAbove_of_small small_range small_Iio omega0_le_of_isSuccLimit opow_one max_le ciSup_le' card_le_card le_of_lt le_max_right
card_opow_le_of_omega0_le_right 📖	mathematical	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder omega0	Cardinal Cardinal.instLE card instPow SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot	—	eq_nat_or_omega0_le LE.le.trans card_le_card opow_le_opow_left LT.lt.le nat_lt_omega0 card_opow_le_of_omega0_le_left le_rfl sup_of_le_right card_nat
card_opow_omega0 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder partialOrder one	card instPow omega0 Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.aleph0	—	card_opow_eq_of_omega0_le_right le_rfl card_omega0 max_comm
lift_card_iSup_le_sum_card 📖	mathematical	—	Cardinal Cardinal.instLE Cardinal.lift card iSup Ordinal ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot Cardinal.sum	—	Cardinal.mk_sigma Cardinal.lift_id' Cardinal.lift_umax Cardinal.lift_mk_le_lift_mk_of_surjective LT.lt.trans_le Set.mem_Iio le_iSup EquivLike.comp_surjective lt_iSup_iff OrderIso.symm_apply_apply
principal_add_omega 📖	mathematical	—	Principal Ordinal add DFunLike.coe OrderEmbedding Preorder.toLE PartialOrder.toPreorder partialOrder instFunLikeOrderEmbedding omega	—	IsInitial.principal_add isInitial_omega omega0_le_omega
principal_add_ord 📖	mathematical	Cardinal Cardinal.instLE Cardinal.aleph0	Principal Ordinal add Cardinal.ord	—	Cardinal.lt_ord card_add Cardinal.add_lt_of_lt
principal_mul_omega 📖	mathematical	—	Principal Ordinal MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass monoidWithZero DFunLike.coe OrderEmbedding Preorder.toLE PartialOrder.toPreorder partialOrder instFunLikeOrderEmbedding omega	—	IsInitial.principal_mul isInitial_omega omega0_le_omega
principal_mul_ord 📖	mathematical	Cardinal Cardinal.instLE Cardinal.aleph0	Principal Ordinal MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass monoidWithZero Cardinal.ord	—	Cardinal.lt_ord card_mul Cardinal.mul_lt_of_lt
principal_opow_omega 📖	mathematical	—	Principal Ordinal instPow DFunLike.coe OrderEmbedding Preorder.toLE PartialOrder.toPreorder partialOrder instFunLikeOrderEmbedding omega	—	eq_zero_or_pos canonicallyOrderedAdd omega_zero principal_opow_omega0 Cardinal.lt_omega_iff_card_lt LE.le.trans_lt card_opow_le max_lt Cardinal.aleph_zero Cardinal.aleph_lt_aleph
principal_opow_ord 📖	mathematical	Cardinal Cardinal.instLE Cardinal.aleph0	Principal Ordinal instPow Cardinal.ord	—	IsInitial.principal_opow isInitial_ord Cardinal.omega0_le_ord

Ordinal.IsInitial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
principal_add 📖	mathematical	Ordinal.IsInitial Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder Ordinal.omega0	Ordinal.Principal Ordinal.add	—	ord_card Ordinal.principal_add_ord Ordinal.aleph0_le_card
principal_mul 📖	mathematical	Ordinal.IsInitial Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder Ordinal.omega0	Ordinal.Principal MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Ordinal.monoidWithZero	—	ord_card Ordinal.principal_mul_ord Ordinal.aleph0_le_card
principal_opow 📖	mathematical	Ordinal.IsInitial Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder Ordinal.omega0	Ordinal.Principal Ordinal.instPow	—	Ordinal.mem_range_omega_iff Ordinal.principal_opow_omega

---

← Back to Index