Skip to content

[Merged by Bors] - feat(Order): add {WithTop,WithBot}.subtypeOrderIso#28192

Closed
wwylele wants to merge 3 commits intoleanprover-community:masterfrom
wwylele:wwylele-hahn-withtopiso
Closed

[Merged by Bors] - feat(Order): add {WithTop,WithBot}.subtypeOrderIso#28192
wwylele wants to merge 3 commits intoleanprover-community:masterfrom
wwylele:wwylele-hahn-withtopiso

Conversation

@wwylele
Copy link
Copy Markdown
Collaborator

@wwylele wwylele commented Aug 10, 2025 •
edited
Loading

Separated from #25970

Open in Gitpod

@wwylele wwylele mentioned this pull request Aug 10, 2025
Closed
7 tasks
@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 10, 2025 •
edited
Loading

PR summary 8623f65b75

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

++ subtypeOrderIso
++ subtypeOrderIso_apply_coe
++ subtypeOrderIso_symm_apply

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

@github-actions github-actions bot added the t-order Order theory label Aug 10, 2025
@wwylele wwylele assigned YaelDillies and unassigned YaelDillies Aug 10, 2025
@wwylele wwylele requested a review from YaelDillies August 10, 2025 19:28
kckennylau
kckennylau reviewed Aug 10, 2025
View reviewed changes
Mathlib/Order/Hom/WithTopBot.lean Outdated
Comment on lines +88 to +90
theorem subtypeOrderIso_symm_apply [DecidableEq α] [PartialOrder α] [OrderTop α]
{a : α} (h : a ≠ ⊤) :
(subtypeOrderIso).symm a = (⟨a, h⟩ : {a : α // a ≠ ⊤}) := by
Copy link
Copy Markdown
Collaborator

@kckennylau kckennylau Aug 10, 2025

Choose a reason for hiding this comment

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

you might want to also state symm_apply_fst

Copy link
Copy Markdown
Collaborator Author

@wwylele wwylele Aug 10, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

I don't think symm_apply_fst works. There is a cast from {a : α // a ≠ ⊤} to WithTop {a : α // a ≠ ⊤} on the right side

kckennylau
kckennylau reviewed Aug 10, 2025
View reviewed changes
kckennylau
kckennylau reviewed Aug 10, 2025
View reviewed changes
alreadydone
alreadydone reviewed Aug 10, 2025
View reviewed changes
YaelDillies
YaelDillies approved these changes Aug 11, 2025
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 delegate

@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 11, 2025

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

@ghost ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Aug 11, 2025
@bryangingechen
Copy link
Copy Markdown
Contributor

bryangingechen commented Aug 14, 2025

Thanks!
bors r+

@ghost 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 Aug 14, 2025
mathlib-bors bot pushed a commit that referenced this pull request Aug 14, 2025
@wwylele
feat(Order): add {WithTop,WithBot}.subtypeOrderIso (#28192)
c163370 
Separated from #25970
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 14, 2025

This PR was included in a batch that successfully built, but then failed to merge into master (it was a non-fast-forward update). It will be automatically retried.

mathlib-bors bot pushed a commit that referenced this pull request Aug 14, 2025
@wwylele
feat(Order): add {WithTop,WithBot}.subtypeOrderIso (#28192)
f0a0e4d 
Separated from #25970
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 14, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Order): add {WithTop,WithBot}.subtypeOrderIso [Merged by Bors] - feat(Order): add {WithTop,WithBot}.subtypeOrderIso Aug 14, 2025
@mathlib-bors mathlib-bors bot closed this Aug 14, 2025
Paul-Lez pushed a commit to Paul-Lez/mathlib4 that referenced this pull request Aug 23, 2025
@wwylele @Paul-Lez
feat(Order): add {WithTop,WithBot}.subtypeOrderIso (leanprover-commun…
af7dd4b 
…ity#28192)

Separated from leanprover-community#25970
pechersky pushed a commit to pechersky/mathlib4 that referenced this pull request Aug 25, 2025
@wwylele @pechersky
feat(Order): add {WithTop,WithBot}.subtypeOrderIso (leanprover-commun…
c5df568 
…ity#28192)

Separated from leanprover-community#25970
@wwylele wwylele deleted the wwylele-hahn-withtopiso branch September 2, 2025 01:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@alreadydone alreadydone alreadydone left review comments

@YaelDillies YaelDillies YaelDillies approved these changes

+1 more reviewer

@kckennylau kckennylau kckennylau left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-order Order theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@wwylele @bryangingechen @alreadydone @YaelDillies @kckennylau