[Merged by Bors] - feat(Order/Partition): add refinement order by Jun2M · Pull Request #36574 · leanprover-community/mathlib4

Jun2M · 2026-03-13T01:58:51Z

This PR expands the API for Partition s

Introduces a PartialOrder (Partition s) instance where partitions are ordered by refinement (P ≤ Q if every part of P is contained in a part of Q). Also adds an OrderTop instance where the top partition consists of the single part s.

Co-authored-by: Peter Nelson [email protected]

github-actions · 2026-03-13T01:59:59Z

PR summary 68e18bf8ed

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ eq_of_not_disjoint
+ eq_or_disjoint
+ existsUnique_of_mem_le
+ exists_le_of_mem_le
+ instance : OrderTop (Partition s)
+ instance : PartialOrder (Partition s)
+ instance : Unique (Partition (⊥ : α))
+ le_def
+ mem_removeBot
+ mem_top_iff
+ ne_bot_of_mem'
+ notMem_of_bot
+ parts_top
+ parts_top_subset
+ top_def
- instance : PartialOrder (Partition s) := .ofSetLike (Partition s) α

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

YaelDillies

This PR is doing too many things at once. Could you move out everything past the refinement order?

Mathlib/Order/Partition/Basic.lean

YaelDillies

Thanks!

maintainer delegate

Mathlib/Order/Partition/Basic.lean

github-actions · 2026-03-23T10:31:07Z

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

pull_request_review, wf_run

YaelDillies

Thanks!

maintainer delegate

Mathlib/Order/Partition/Basic.lean

github-actions · 2026-03-23T17:54:07Z

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

pull_request_review, wf_run

Co-authored-by: Yaël Dillies <[email protected]>

bryangingechen

Thanks!
bors r+

This PR expands the API for `Partition s` Introduces a `PartialOrder (Partition s)` instance where partitions are ordered by refinement (`P ≤ Q` if every part of `P` is contained in a part of `Q`). Also adds an `OrderTop` instance where the top partition consists of the single part `s`. Co-authored-by: Peter Nelson <[email protected]>

mathlib-bors · 2026-03-26T23:25:15Z

Pull request successfully merged into master.

Build succeeded:

This PR expands the API for `Partition s` Introduces a `PartialOrder (Partition s)` instance where partitions are ordered by refinement (`P ≤ Q` if every part of `P` is contained in a part of `Q`). Also adds an `OrderTop` instance where the top partition consists of the single part `s`. Co-authored-by: Peter Nelson <[email protected]>

init

e0a36e8

github-actions bot added the t-order Order theory label Mar 13, 2026

Jun2M added 5 commits March 12, 2026 22:09

Simp NF fix

793fd00

SimpNF fix 2

5a2c13f

IsRepFun

34dfd75

fix typo

c559334

u as ground set

92e80ec

Jun2M mentioned this pull request Mar 15, 2026

feat(Order/Partition): every partition has IsRepFun #36691

Open

3 tasks

mathlib-triage bot assigned YaelDillies Mar 22, 2026

YaelDillies reviewed Mar 22, 2026

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 22, 2026

update

45b564c

Jun2M added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Mar 22, 2026

Jun2M added 2 commits March 22, 2026 13:01

Merge branch 'master' into partition-repfun

ef36a02

Break into different PRs

67fb2a9

This was referenced Mar 22, 2026

feat(Order/Partition): add Rel, relation induced by partition on Set #36991

Open

feat(Order/Partition): add IsRepFun #36993

Open

Jun2M changed the title ~~feat(Order/Partition): add refinement order and set partition API~~ feat(Order/Partition): add refinement order Mar 22, 2026

doc rm

0366ce7

Jun2M removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 22, 2026

YaelDillies approved these changes Mar 23, 2026

View reviewed changes

Mathlib/Order/Partition/Basic.lean Outdated Show resolved Hide resolved

mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Mar 23, 2026

YaelDillies removed their assignment Mar 23, 2026

top_def

050e9bc

YaelDillies approved these changes Mar 23, 2026

View reviewed changes

Mathlib/Order/Partition/Basic.lean Outdated Show resolved Hide resolved

Update Mathlib/Order/Partition/Basic.lean

38db05a

Co-authored-by: Yaël Dillies <[email protected]>

mathlib-triage bot assigned bryangingechen Mar 24, 2026

bryangingechen approved these changes Mar 26, 2026

View reviewed changes

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 26, 2026

mathlib-bors bot changed the title ~~feat(Order/Partition): add refinement order~~ [Merged by Bors] - feat(Order/Partition): add refinement order Mar 26, 2026

mathlib-bors bot closed this Mar 26, 2026

Conversation

Jun2M commented Mar 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Mar 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 68e18bf8ed

Import changes for modified files

Declarations diff

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

github-actions bot commented Mar 23, 2026

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

github-actions bot commented Mar 23, 2026

Uh oh!

bryangingechen left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Mar 26, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Jun2M commented Mar 13, 2026 •

edited

Loading

github-actions bot commented Mar 13, 2026 •

edited

Loading