Skip to content

[Merged by Bors] - feat: a cofinal set has a cofinal subset of order type (cof α).ord#39789

Closed
vihdzp wants to merge 9 commits into
leanprover-community:masterfrom
vihdzp:coflemmas
Closed

[Merged by Bors] - feat: a cofinal set has a cofinal subset of order type (cof α).ord#39789
vihdzp wants to merge 9 commits into
leanprover-community:masterfrom
vihdzp:coflemmas

Conversation

@vihdzp

@vihdzp vihdzp commented May 24, 2026

Copy link
Copy Markdown
Collaborator

Open in Gitpod

@vihdzp vihdzp added the t-set-theory Set theory label May 24, 2026
@vihdzp
vihdzp requested a review from YaelDillies May 24, 2026 20:37
@github-actions

github-actions Bot commented May 24, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary 9b5051b113

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ _root_.OrderIso.ordinalType_congr
+ _root_.RelIso.ordinalType_congr
+ cof_eq_of_isCofinal
+ exists_ord_cof_eq_of_isCofinal
- _root_.RelIso.ordinal_type_eq

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.
No changes to weak technical debt.

@github-actions github-actions Bot added large-import Automatically added label for PRs with a significant increase in transitive imports file-removed A Lean module was (re)moved without a `deprecated_module` annotation labels May 25, 2026
@github-actions github-actions Bot removed large-import Automatically added label for PRs with a significant increase in transitive imports file-removed A Lean module was (re)moved without a `deprecated_module` annotation labels May 25, 2026
YaelDillies
YaelDillies reviewed May 25, 2026
View reviewed changes
Comment thread Mathlib/SetTheory/Ordinal/Basic.lean Outdated
YaelDillies
YaelDillies reviewed May 25, 2026
View reviewed changes
Comment thread Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean Outdated
vihdzp and others added 2 commits May 25, 2026 12:33
@vihdzp @YaelDillies
Update Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
e7d58c7 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@vihdzp
fix
0ebcdb1
@mathlib-merge-conflicts mathlib-merge-conflicts 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 May 26, 2026
@mathlib-merge-conflicts

mathlib-merge-conflicts Bot commented May 26, 2026

Copy link
Copy Markdown

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 26, 2026
YaelDillies
YaelDillies approved these changes May 26, 2026
View reviewed changes

@YaelDillies YaelDillies left a comment

Copy link
Copy Markdown
Contributor

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

github-actions Bot commented May 26, 2026

Copy link
Copy Markdown

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

@mathlib-triage mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label May 26, 2026
@riccardobrasca

riccardobrasca commented Jun 3, 2026

Copy link
Copy Markdown
Member

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 Jun 3, 2026
mathlib-bors Bot pushed a commit that referenced this pull request Jun 3, 2026
@vihdzp
feat: a cofinal set has a cofinal subset of order type (cof α).ord (#…
cadd914 
…39789)
@mathlib-bors

mathlib-bors Bot commented Jun 3, 2026

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title feat: a cofinal set has a cofinal subset of order type (cof α).ord [Merged by Bors] - feat: a cofinal set has a cofinal subset of order type (cof α).ord Jun 3, 2026
@mathlib-bors mathlib-bors Bot closed this Jun 3, 2026
Bergschaf pushed a commit to Bergschaf/mathlib4 that referenced this pull request Jun 3, 2026
@vihdzp @Bergschaf
feat: a cofinal set has a cofinal subset of order type (cof α).ord (l…
170fdb7 
…eanprover-community#39789)
ReemMelamed pushed a commit to ReemMelamed/mathlib4 that referenced this pull request Jun 20, 2026
@vihdzp @ReemMelamed
feat: a cofinal set has a cofinal subset of order type (cof α).ord (l…
254b456 
…eanprover-community#39789)
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