Commit 2025-10-29 00:35 7c26ba6c

View on Github →

feat(SetTheory): more API for HasCardinalLT (#30633) We add stability lemmas for HasCardinalLT X κ for sigma types, binary products, etc when κ is regular (or at least infinite).

Estimated changes

Modified Mathlib/SetTheory/Cardinal/HasCardinalLT.lean

added theorem hasCardinalLT_iUnion

added theorem hasCardinalLT_lift_iff

added theorem hasCardinalLT_of_finite

added theorem hasCardinalLT_prod'

added theorem hasCardinalLT_prod

added theorem hasCardinalLT_sigma'

added theorem hasCardinalLT_sigma

added theorem hasCardinalLT_subtype_iSup

added theorem hasCardinalLT_subtype_max

added theorem hasCardinalLT_ulift_iff

added theorem hasCardinalLT_union

Modified Mathlib/SetTheory/Cardinal/Regular.lean

added theorem Cardinal.IsRegular.lift

added theorem Cardinal.isRegular_lift_iff