Skip to content

[Merged by Bors] - feat: if s is bounded by a and has size below cof a then sSup s < a#37015

Closed
vihdzp wants to merge 23 commits intoleanprover-community:masterfrom
vihdzp:cof_normal4
Closed

[Merged by Bors] - feat: if s is bounded by a and has size below cof a then sSup s < a#37015
vihdzp wants to merge 23 commits intoleanprover-community:masterfrom
vihdzp:cof_normal4

Conversation

@vihdzp
Copy link
Copy Markdown
Collaborator

@vihdzp vihdzp commented Mar 23, 2026 •
edited
Loading

Some of these lemmas existed already as lemmas on lsub, but the new versions have more general universes. A follow-up PR will deprecate many of the lsub lemmas.

Open in Gitpod

@github-actions github-actions bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 23, 2026
@github-actions github-actions bot added t-set-theory Set theory and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Mar 23, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 23, 2026 •
edited
Loading

PR summary 8a12e93279

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ _root_.Cardinal.iSup_lt_of_lt_cof_ord
+ _root_.Cardinal.lift_iSup_lt_of_lt_cof_ord
+ _root_.Cardinal.sSup_lt_of_lt_cof_ord
+ cof_iSup_add_one_le
+ cof_lift_iSup_add_one_le
+ iSup_add_one_lt_of_lt_cof
+ iSup_lt_of_lt_cof
+ lift_iSup_add_one_lt_of_lt_cof
+ lift_iSup_lt_of_lt_cof
+ sSup_add_one_lt_of_lt_cof
+ sSup_lt_of_lt_cof

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

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

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

No changes to technical debt.

You can run this locally as

./scripts/reporting/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 vihdzp mentioned this pull request Mar 23, 2026
Closed
3 tasks
@mathlib-dependent-issues mathlib-dependent-issues bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 23, 2026
@vihdzp vihdzp mentioned this pull request Mar 23, 2026
Open
3 tasks
@vihdzp vihdzp requested a review from YaelDillies March 23, 2026 10:01
@vihdzp vihdzp removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 23, 2026
@mathlib-dependent-issues
Copy link
Copy Markdown

mathlib-dependent-issues bot commented Mar 23, 2026

This PR/issue depends on:

YaelDillies
YaelDillies reviewed Mar 23, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You use .ord.cof a lot. Does this mean we should have Cardinal.cof, eg as an abbrev for Ordinal.cof \comp Cardinal.ord? Is cofinality of a cardinal an informal concept?

@vihdzp
Copy link
Copy Markdown
Collaborator Author

vihdzp commented Mar 23, 2026

One does in fact often talk about the cofinality of a cardinal (remember that set theorists like to conflate ordinals and cardinals). We could define Cardinal.cof, but I don't think it would have much benefit. The boilerplate we'd have to write to keep the Ordinal.cof and Cardinal.cof APIs in sync surely outweighs the characters we save from writing c.cof instead of c.ord.cof.

@YaelDillies
Copy link
Copy Markdown
Contributor

YaelDillies commented Mar 23, 2026

I was thinking it could be an abbrev with little API. If you disagree, please make sure you use cof_ord in your lemma names

@vihdzp
Copy link
Copy Markdown
Collaborator Author

vihdzp commented Mar 23, 2026

I was thinking it could be an abbrev with little API.

I think that would cause confusion. e.g. imagine searching the lemma cof_aleph0 : cof ℵ₀ = ℵ₀ and not being able to find it, because what you actually needed to do was rewrite with ord_aleph0 : ord ℵ₀ = ω followed by cof_omega0 : cof ω = ℵ₀.

If you disagree, please make sure you use cof_ord in your lemma names

Will do! Doing this also resolves the name clashes between the ordinal and cardinal lemmas.

YaelDillies
YaelDillies approved these changes Mar 23, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks! 🚀

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 23, 2026

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

pull_request_review, wf_run

@mathlib-triage mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Mar 23, 2026
@b-mehta
Copy link
Copy Markdown
Contributor

b-mehta commented Mar 24, 2026

You use .ord.cof a lot. Does this mean we should have Cardinal.cof, eg as an abbrev for Ordinal.cof \comp Cardinal.ord? Is cofinality of a cardinal an informal concept?

FWIW, I view the cofinality of a cardinal as an important informal concept, and so IMO we should use cof rather than cof_ord in lemma names for readability (the ord is not doing anything interesting or relevant, it's just there to make things type-correct!)

b-mehta
b-mehta reviewed Mar 24, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@b-mehta b-mehta left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

bors merge

@mathlib-triage mathlib-triage bot 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 Mar 24, 2026
mathlib-bors bot pushed a commit that referenced this pull request Mar 24, 2026
@vihdzp
feat: if s is bounded by a and has size below cof a then `sSup …
dae701a 
…s < a` (#37015)

Some of these lemmas existed already as lemmas on `lsub`, but the new versions have more general universes. A follow-up PR will deprecate many of the `lsub` lemmas.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 24, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: if s is bounded by a and has size below cof a then sSup s < a [Merged by Bors] - feat: if s is bounded by a and has size below cof a then sSup s < a Mar 24, 2026
@mathlib-bors mathlib-bors bot closed this Mar 24, 2026
justus-springer pushed a commit to justus-springer/mathlib4 that referenced this pull request Mar 28, 2026
@vihdzp @justus-springer
feat: if s is bounded by a and has size below cof a then `sSup …
27168e1 
…s < a` (leanprover-community#37015)

Some of these lemmas existed already as lemmas on `lsub`, but the new versions have more general universes. A follow-up PR will deprecate many of the `lsub` lemmas.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@b-mehta b-mehta b-mehta left review comments

@YaelDillies YaelDillies YaelDillies approved these changes

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-set-theory Set theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@vihdzp @YaelDillies @b-mehta