Commit 2025-10-22 19:38 df375c23

View on Github →

feat(SetTheory/Cardinal): generalize and rename theorems on Cardinal.sum (#29351) Some theorems on Cardinal.sum f are taking f : ι → Cardinal.{max u v}, which can be generalized to f : ι → Cardinal.{v}. Also rename sum_le_iSup_lift, sum_eq_iSup_lift etc. to reflect their signatures in names.

Estimated changes

Modified Mathlib/Data/W/Cardinal.lean

Modified Mathlib/ModelTheory/Encoding.lean

Modified Mathlib/SetTheory/Cardinal/Arithmetic.lean

deleted theorem Cardinal.sum_eq_iSup

deleted theorem Cardinal.sum_eq_iSup_lift

added theorem Cardinal.sum_eq_iSup_of_lift_mk_le_iSup

added theorem Cardinal.sum_eq_iSup_of_mk_le_iSup

added theorem Cardinal.sum_eq_lift_iSup_of_lift_mk_le_lift_iSup

Modified Mathlib/SetTheory/Cardinal/Basic.lean

added theorem Cardinal.lift_iSup_le_sum

deleted theorem Cardinal.sum_le_iSup

deleted theorem Cardinal.sum_le_iSup_lift

added theorem Cardinal.sum_le_lift_mk_mul_iSup

added theorem Cardinal.sum_le_lift_mk_mul_iSup_lift

added theorem Cardinal.sum_le_mk_mul_iSup

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Modified Mathlib/SetTheory/Cardinal/Defs.lean

added theorem Cardinal.lift_power_sum

modified theorem Cardinal.power_sum

Modified Mathlib/SetTheory/Cardinal/Order.lean

modified theorem Cardinal.le_sum

added theorem Cardinal.lift_le_sum

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean

Modified Mathlib/SetTheory/Cardinal/Pigeonhole.lean

Modified Mathlib/SetTheory/Cardinal/Regular.lean