[Merged by Bors] - feat(SetTheory/Cardinal): generalize and rename theorems on `Cardinal.sum` by staroperator · Pull Request #29351 · leanprover-community/mathlib4

staroperator · 2025-09-04T17:59:58Z

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.

github-actions · 2025-09-04T18:01:07Z

PR summary 5c98c223ad

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ lift_iSup_le_sum
+ lift_le_sum
+ lift_power_sum
+ sum_eq_iSup_of_lift_mk_le_iSup
+ sum_eq_iSup_of_mk_le_iSup
+ sum_eq_lift_iSup_of_lift_mk_le_lift_iSup
+ sum_le_lift_mk_mul_iSup
+ sum_le_lift_mk_mul_iSup_lift
+ sum_le_mk_mul_iSup

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

vihdzp

Thank you!

Mathlib/SetTheory/Cardinal/Basic.lean

staroperator · 2025-09-05T13:12:50Z

Mathlib/SetTheory/Cardinal/Regular.lean

    (∀ i, f i < c) → iSup f < c :=
  iSup_lt (by rwa [hc.cof_eq])

+theorem sum_lt_lift_of_isRegular' {ι} {f : ι → Cardinal} {c : Cardinal} (hc : IsRegular c)


This name is a bit scary. Any suggestions are welcome!

Renamed to IsRegular.sum_lt_of_lift_mk_lt_of_lift_lt. We should also rename other _of_isRegular theorems to IsRegular. in the same file in future.

I have reverted those renames. I plan to do that with generalization of other IsRegular theorems together, in the future.

alreadydone

Thanks 🎉
maintainer delegate

(and please merge master)

Mathlib/SetTheory/Cardinal/Basic.lean

Mathlib/SetTheory/Cardinal/Defs.lean

github-actions · 2025-10-18T11:06:29Z

🚀 Pull request has been placed on the maintainer queue by alreadydone.

Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

riccardobrasca · 2025-10-22T09:06:22Z

Thanks!

bors merge

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

mathlib-bors · 2025-10-22T09:45:16Z

Build failed (retrying...):

Post-Build Step

alreadydone · 2025-10-22T09:48:30Z

It would be nicer if you used merge rather than rebase to update the branch, since the comparison shows too large a diff with rebase. It took me a while to figure out the changes after my review are the four commits starting from 4fe67f2.

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

mathlib-bors · 2025-10-22T11:41:24Z

Build failed (retrying...):

Post-Build Step

staroperator · 2025-10-22T13:09:55Z

It would be nicer if you used merge rather than rebase to update the branch, since the comparison shows too large a diff with rebase. It took me a while to figure out the changes after my review are the four commits starting from 4fe67f2.

Emm, I personally strongly prefer rebase because it makes neat commit history. Though what you said makes sense; let me try to do merge instead of rebase in my other PRs after someone has reviewed.

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

riccardobrasca · 2025-10-22T13:18:23Z

It would be nicer if you used merge rather than rebase to update the branch, since the comparison shows too large a diff with rebase. It took me a while to figure out the changes after my review are the four commits starting from 4fe67f2.

Emm, I personally strongly prefer rebase because it makes neat commit history. Though what you said makes sense; let me try to do merge instead of rebase in my other PRs after someone has reviewed.

We squash merge, so the history of your branch does not really matter.

staroperator · 2025-10-22T13:26:02Z

It would be nicer if you used merge rather than rebase to update the branch, since the comparison shows too large a diff with rebase. It took me a while to figure out the changes after my review are the four commits starting from 4fe67f2.

Emm, I personally strongly prefer rebase because it makes neat commit history. Though what you said makes sense; let me try to do merge instead of rebase in my other PRs after someone has reviewed.

We squash merge, so the history of your branch does not really matter.

That's right, keeping a neat commit history is my personal aestheticism 😃 Especially when merge does not allow deleting commits from dependency PRs.

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

mathlib-bors · 2025-10-22T14:15:26Z

Build failed (retrying...):

Post-Build Step

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

mathlib-bors · 2025-10-22T17:32:40Z

Build failed (retrying...):

Post-Build Step

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

mathlib-bors · 2025-10-22T20:30:18Z

Pull request successfully merged into master.

Build succeeded:

….sum` (leanprover-community#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.

staroperator added the t-set-theory Set theory label Sep 4, 2025

vihdzp approved these changes Sep 5, 2025

View reviewed changes

Mathlib/SetTheory/Cardinal/Basic.lean Outdated Show resolved Hide resolved

Mathlib/SetTheory/Cardinal/Basic.lean Outdated Show resolved Hide resolved

staroperator commented Sep 5, 2025

View reviewed changes

staroperator mentioned this pull request Sep 5, 2025

chore(SetTheory/Cardinal/Basic): generalize universes of sum_le_iSup_lift #21856

Closed

staroperator changed the title ~~feat(SetTheory/Cardinal): generalize some theorems on Cardinal.sum~~ feat(SetTheory/Cardinal): generalize and rename theorems on Cardinal.sum Sep 6, 2025

staroperator mentioned this pull request Sep 7, 2025

[Merged by Bors] - feat(SetTheory/ZFC): card (V_ o) = preBeth o #29393

Closed

3 tasks

leanprover-community-bot-assistant assigned alreadydone Sep 30, 2025

alreadydone approved these changes Oct 18, 2025

View reviewed changes

Mathlib/SetTheory/Cardinal/Basic.lean Outdated Show resolved Hide resolved

Mathlib/SetTheory/Cardinal/Defs.lean Outdated Show resolved Hide resolved

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Oct 18, 2025

staroperator and others added 9 commits October 18, 2025 21:48

add

38de26b

Apply suggestions from code review

b770f86

Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>

improve

321f0a0

rename

b5957e0

add lift_iSup_le_sum

79977e1

add sum_eq_lift_iSup_of_lift_mk_le_lift_iSup

93c3d6b

Update Mathlib/SetTheory/Cardinal/Basic.lean

4fe67f2

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

add universes

bd3b034

revert IsRegular

3f957a8

staroperator force-pushed the cardinal_refactor branch from 9c3b735 to 3f957a8 Compare October 19, 2025 01:58

fix alias

4fe30f9

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Oct 22, 2025

alreadydone approved these changes Oct 22, 2025

View reviewed changes

mathlib-bors bot changed the title ~~feat(SetTheory/Cardinal): generalize and rename theorems on Cardinal.sum~~ [Merged by Bors] - feat(SetTheory/Cardinal): generalize and rename theorems on Cardinal.sum Oct 22, 2025

mathlib-bors bot closed this Oct 22, 2025

Conversation

staroperator commented Sep 4, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Sep 4, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 5c98c223ad

Import changes for modified files

Declarations diff

Uh oh!

vihdzp left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

staroperator Sep 5, 2025

Choose a reason for hiding this comment

Uh oh!

staroperator Sep 6, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

staroperator Oct 19, 2025

Choose a reason for hiding this comment

Uh oh!

alreadydone left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented Oct 18, 2025

Uh oh!

riccardobrasca commented Oct 22, 2025

Uh oh!

mathlib-bors bot commented Oct 22, 2025

Uh oh!

alreadydone commented Oct 22, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib-bors bot commented Oct 22, 2025

Uh oh!

staroperator commented Oct 22, 2025

Uh oh!

riccardobrasca commented Oct 22, 2025

Uh oh!

staroperator commented Oct 22, 2025

Uh oh!

mathlib-bors bot commented Oct 22, 2025

Uh oh!

mathlib-bors bot commented Oct 22, 2025

Uh oh!

mathlib-bors bot commented Oct 22, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

staroperator commented Sep 4, 2025 •

edited

Loading

github-actions bot commented Sep 4, 2025 •

edited

Loading

staroperator Sep 6, 2025 •

edited

Loading

alreadydone left a comment •

edited

Loading

alreadydone commented Oct 22, 2025 •

edited

Loading