Skip to content

[Merged by Bors] - refactor: generalise compact from CompleteLattice to PartialOrder#33061

Closed
edwin1729 wants to merge 2 commits intoleanprover-community:masterfrom
edwin1729:unify-compact
Closed

[Merged by Bors] - refactor: generalise compact from CompleteLattice to PartialOrder#33061
edwin1729 wants to merge 2 commits intoleanprover-community:masterfrom
edwin1729:unify-compact

Conversation

@edwin1729
Copy link
Copy Markdown
Contributor

@edwin1729 edwin1729 commented Dec 18, 2025 •
edited by bryangingechen
Loading

IsCompactElement assumes a CompleteLattice structure on the type for which it is defined. But a PartialOrder will suffice and this is the textbook definition of compact https://en.wikipedia.org/wiki/Compact_element.
Also it is currently defined in a non-standard way. The standard definition uses directed sets. Changing this has
indeed simplified most proofs by removing an rw into this more standard form.

Note to reviewers: moving IsCompactElement out of the CompleteLattice namespace caused the loss of being able to use dot notation here and here. Would like help fixing that

Open in Gitpod

@github-actions github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Dec 18, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Dec 18, 2025 •
edited
Loading

PR summary 0bc483ae44

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ isCompactElement_iff_exists_le_iSup_of_le_iSup.{u}
+ isCompactElement_iff_exists_le_sSup_of_le_sSup
- isCompactElement_iff.{u}

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

@edwin1729 edwin1729 mentioned this pull request Dec 18, 2025
Open
1 task
@edwin1729 edwin1729 marked this pull request as ready for review December 18, 2025 20:45
@edwin1729
Copy link
Copy Markdown
Contributor Author

edwin1729 commented Dec 18, 2025

@b-mehta requesting review

plp127
plp127 reviewed Dec 19, 2025
View reviewed changes
b-mehta
b-mehta reviewed Dec 19, 2025
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.

The loss of dot notation is because the def's name used to be a prefix of the relevant lemmas, but the new name isn't any more. You could move the lemmas out of CompleteLattice, which might make sense to do, currently most lemmas about CompleteLattice outside this file aren't in that namespace.
Nice work though!

@edwin1729 edwin1729 changed the title Generalise compact from CompleteLattice to PartialOrder refactor: generalise compact from CompleteLattice to PartialOrder Dec 19, 2025
@jcommelin jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 19, 2025
@edwin1729
Copy link
Copy Markdown
Contributor Author

edwin1729 commented Dec 23, 2025

The loss of dot notation is because the def's name used to be a prefix of the relevant lemmas, but the new name isn't any more. You could move the lemmas out of CompleteLattice, which might make sense to do, currently most lemmas about CompleteLattice outside this file aren't in that namespace. Nice work though!

I think I will just leave it as is. Since dot notation could be used if future lemmas where placed in the CompleteLattice namespace

@edwin1729 edwin1729 force-pushed the unify-compact branch 2 times, most recently from 0b80fbd to b7cef19 Compare December 24, 2025 13:33
@edwin1729 edwin1729 requested a review from b-mehta December 25, 2025 19:52
@edwin1729
Copy link
Copy Markdown
Contributor Author

edwin1729 commented Jan 6, 2026

Just a reminder that this PR is ready for review, and all comments have been addressed. @b-mehta

b-mehta
b-mehta reviewed Jan 15, 2026
View reviewed changes
@b-mehta b-mehta added auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jan 15, 2026
@ghost
Copy link
Copy Markdown

ghost commented Jan 15, 2026

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Jan 15, 2026
mathlib-bors bot pushed a commit that referenced this pull request Jan 15, 2026
@edwin1729
refactor: generalise compact from CompleteLattice to PartialOrder (#3…
26299a5 
…3061)

`IsCompactElement` assumes a `CompleteLattice` structure on the type for which it is defined. But a `PartialOrder` will suffice and this is the textbook definition of compact https://en.wikipedia.org/wiki/Compact_element.
Also it is currently defined in a non-standard way. The standard definition uses directed sets. Changing this has
indeed simplified most proofs by removing an `rw` into this more standard form.

Co-authored-by: Edwin Fernando <[email protected]>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 15, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title refactor: generalise compact from CompleteLattice to PartialOrder [Merged by Bors] - refactor: generalise compact from CompleteLattice to PartialOrder Jan 15, 2026
@mathlib-bors mathlib-bors bot closed this Jan 15, 2026
@adomani adomani mentioned this pull request Jan 16, 2026
Open
eliasjudin pushed a commit to eliasjudin/mathlib4 that referenced this pull request Jan 18, 2026
@edwin1729 @eliasjudin
refactor: generalise compact from CompleteLattice to PartialOrder (le…
6037f40 
…anprover-community#33061)

`IsCompactElement` assumes a `CompleteLattice` structure on the type for which it is defined. But a `PartialOrder` will suffice and this is the textbook definition of compact https://en.wikipedia.org/wiki/Compact_element.
Also it is currently defined in a non-standard way. The standard definition uses directed sets. Changing this has
indeed simplified most proofs by removing an `rw` into this more standard form.

Co-authored-by: Edwin Fernando <[email protected]>
bilichboris pushed a commit to bilichboris/mathlib4 that referenced this pull request Jan 18, 2026
@edwin1729 @bilichboris
refactor: generalise compact from CompleteLattice to PartialOrder (le…
c09d203 
…anprover-community#33061)

`IsCompactElement` assumes a `CompleteLattice` structure on the type for which it is defined. But a `PartialOrder` will suffice and this is the textbook definition of compact https://en.wikipedia.org/wiki/Compact_element.
Also it is currently defined in a non-standard way. The standard definition uses directed sets. Changing this has
indeed simplified most proofs by removing an `rw` into this more standard form.

Co-authored-by: Edwin Fernando <[email protected]>
goliath-klein pushed a commit to PrParadoxy/mathlib4 that referenced this pull request Jan 24, 2026
@edwin1729 @goliath-klein
refactor: generalise compact from CompleteLattice to PartialOrder (le…
5544d4c 
…anprover-community#33061)

`IsCompactElement` assumes a `CompleteLattice` structure on the type for which it is defined. But a `PartialOrder` will suffice and this is the textbook definition of compact https://en.wikipedia.org/wiki/Compact_element.
Also it is currently defined in a non-standard way. The standard definition uses directed sets. Changing this has
indeed simplified most proofs by removing an `rw` into this more standard form.

Co-authored-by: Edwin Fernando <[email protected]>
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

@plp127 plp127 plp127 left review comments

Assignees

No one assigned

Labels

auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@edwin1729 @b-mehta @plp127 @jcommelin