Commit 2024-12-16 00:47 dd3f45ba

View on Github →

feat(SetTheory/Ordinal/Arithmetic): (sInf sᶜ).card ≤ #s (#18780) The cardinality of the least ordinal not in a set is at most the cardinality of the set.

Estimated changes

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

added theorem Ordinal.card_sInf_range_compl_le

added theorem Ordinal.card_sInf_range_compl_le_lift

added theorem Ordinal.lift_card_sInf_compl_le