Commit 2024-12-16 00:26 9e107689

View on Github →

feat(SetTheory/Cardinal/Arithmetic): cardinality of ordinal exponential (#17813) We prove variations on (a ^ b).card = max a.card b.card.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

added theorem Cardinal.lt_omega_iff_card_lt

Modified Mathlib/SetTheory/Cardinal/Arithmetic.lean

added theorem Ordinal.IsInitial.principal_opow

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.principal_opow_omega

added theorem Ordinal.principal_opow_ord

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

added theorem Ordinal.eq_nat_or_omega0_le

Modified Mathlib/SetTheory/Ordinal/Principal.lean