Commit 2025-03-17 11:54 53b17b6a

View on Github →

refactor(SetTheory/Cardinal/Ordinal): move results (#21857) We move the latter third of SetTheory.Cardinal.Arithmetic to its own file, so that cardinal arithmetic doesn't need to import e.g. ordinal exponentiation or anything too fancy about ordinals.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Card.lean

Modified Mathlib/SetTheory/Cardinal/Arithmetic.lean

deleted theorem Cardinal.mk_iUnion_Ordinal_le_of_le

deleted theorem Cardinal.mk_iUnion_Ordinal_lift_le_of_le

deleted theorem Cardinal.principal_add_aleph

deleted theorem Ordinal.IsInitial.principal_add

deleted theorem Ordinal.IsInitial.principal_mul

deleted theorem Ordinal.IsInitial.principal_opow

deleted theorem Ordinal.card_iSup_Iio_le_card_mul_iSup

deleted theorem Ordinal.card_iSup_Iio_le_sum_card

deleted theorem Ordinal.card_iSup_le_sum_card

deleted theorem Ordinal.card_omega0_opow

deleted theorem Ordinal.card_opow_eq_of_omega0_le_left

deleted theorem Ordinal.card_opow_eq_of_omega0_le_right

deleted theorem Ordinal.card_opow_le

deleted theorem Ordinal.card_opow_le_of_omega0_le_left

deleted theorem Ordinal.card_opow_le_of_omega0_le_right

deleted theorem Ordinal.card_opow_omega0

deleted theorem Ordinal.lift_card_iSup_le_sum_card

deleted theorem Ordinal.principal_add_omega

deleted theorem Ordinal.principal_add_ord

deleted theorem Ordinal.principal_mul_omega

deleted theorem Ordinal.principal_mul_ord

deleted theorem Ordinal.principal_opow_omega

deleted theorem Ordinal.principal_opow_ord

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Created Mathlib/SetTheory/Cardinal/Ordinal.lean

added theorem Cardinal.mk_iUnion_Ordinal_le_of_le

added theorem Cardinal.mk_iUnion_Ordinal_lift_le_of_le

added theorem Cardinal.principal_add_aleph

added theorem Ordinal.IsInitial.principal_add

added theorem Ordinal.IsInitial.principal_mul

added theorem Ordinal.IsInitial.principal_opow

added theorem Ordinal.card_iSup_Iio_le_card_mul_iSup

added theorem Ordinal.card_iSup_Iio_le_sum_card

added theorem Ordinal.card_iSup_le_sum_card

added theorem Ordinal.card_omega0_opow

added theorem Ordinal.card_opow_eq_of_omega0_le_left

added theorem Ordinal.card_opow_eq_of_omega0_le_right

added theorem Ordinal.card_opow_le

added theorem Ordinal.card_opow_le_of_omega0_le_left

added theorem Ordinal.card_opow_le_of_omega0_le_right

added theorem Ordinal.card_opow_omega0

added theorem Ordinal.lift_card_iSup_le_sum_card

added theorem Ordinal.principal_add_omega

added theorem Ordinal.principal_add_ord

added theorem Ordinal.principal_mul_omega

added theorem Ordinal.principal_mul_ord

added theorem Ordinal.principal_opow_omega

added theorem Ordinal.principal_opow_ord