Skip to content

[Merged by Bors] - feat: cof (ω_ (o + 1)) = ℵ_ (o + 1)#37020

Closed
vihdzp wants to merge 9 commits intoleanprover-community:masterfrom
vihdzp:cofsucc
Closed

[Merged by Bors] - feat: cof (ω_ (o + 1)) = ℵ_ (o + 1)#37020
vihdzp wants to merge 9 commits intoleanprover-community:masterfrom
vihdzp:cofsucc

Conversation

@vihdzp
Copy link
Copy Markdown
Collaborator

@vihdzp vihdzp commented Mar 23, 2026

Open in Gitpod

@vihdzp vihdzp added easy < 20s of review time. See the lifecycle page for guidelines. t-set-theory Set theory labels Mar 23, 2026
@github-actions
Copy link
Copy Markdown

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

PR summary 04c569f2fc

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ cof_omega_add_one
+ cof_omega_one
+ cof_preOmega_add_one
+ isRegular_aleph_add_one
+ isRegular_preAleph_add_one
+ succ_aleph
+ succ_preAleph

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 removed the easy < 20s of review time. See the lifecycle page for guidelines. label Mar 23, 2026
This was referenced Mar 23, 2026
Open
Closed
@vihdzp vihdzp requested a review from YaelDillies March 27, 2026 08:26
YaelDillies
YaelDillies reviewed Mar 27, 2026
View reviewed changes
Mathlib/SetTheory/Cardinal/Regular.lean
Comment on lines +117 to +118
theorem cof_preOmega_add_one {o : Ordinal} (h : ω ≤ o) :
(preOmega (o + 1)).cof = preAleph (o + 1) := by
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies Mar 27, 2026

Choose a reason for hiding this comment

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

Couldn't you generalise this syntactically to

Suggested change
theorem cof_preOmega_add_one {o : Ordinal} (h : ω ≤ o) :
(preOmega (o + 1)).cof = preAleph (o + 1) := by
theorem cof_preOmega_add_one {o : Ordinal} (h : ω ≤ o) (ho : \not IsLimit o) :
(preOmega o).cof = preAleph o := by

? Same everywhere else

Copy link
Copy Markdown
Collaborator Author

@vihdzp vihdzp Mar 27, 2026

Choose a reason for hiding this comment

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

I don't know if that's all that useful? I don't see what kind of circumstance would give you a ¬ IsSuccPrelimit x hypothesis that you wouldn't immediately try to use to rewrite x = y + 1.

Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies Mar 27, 2026

Choose a reason for hiding this comment

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

As you wish

@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 27, 2026
YaelDillies
YaelDillies approved these changes Mar 27, 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

@YaelDillies YaelDillies removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 27, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 27, 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 27, 2026
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Mar 30, 2026

Thanks!

bors merge
Thanks!

bors merge

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 30, 2026

Already running a review

@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 30, 2026
mathlib-bors bot pushed a commit that referenced this pull request Mar 30, 2026
@vihdzp
feat: cof (ω_ (o + 1)) = ℵ_ (o + 1) (#37020)
0a6afa8
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 30, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: cof (ω_ (o + 1)) = ℵ_ (o + 1) [Merged by Bors] - feat: cof (ω_ (o + 1)) = ℵ_ (o + 1) Mar 30, 2026
@mathlib-bors mathlib-bors bot closed this Mar 30, 2026
aditya-ramabadran pushed a commit to aditya-ramabadran/mathlib4 that referenced this pull request Apr 1, 2026
@vihdzp @aditya-ramabadran
feat: cof (ω_ (o + 1)) = ℵ_ (o + 1) (leanprover-community#37020)
65aaa77
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@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 @riccardobrasca @YaelDillies