Skip to content

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

Open
Jun2M wants to merge 12 commits intoleanprover-community:masterfrom
Jun2M:PartitionSet
Open

feat(Order/Partition): add Rel, relation induced by partition on Set#36991
Jun2M wants to merge 12 commits intoleanprover-community:masterfrom
Jun2M:PartitionSet

Conversation

@Jun2M
Copy link
Copy Markdown
Collaborator

@Jun2M Jun2M commented Mar 22, 2026 •
edited
Loading

Main changes:

  • Set partition API: Adds a Set section with various useful lemmas for working with partitions of sets.
  • Induced relation: Defines Partition.Rel, a transitive and symmetric binary relation (partial equivalence relation) induced by a partition of a set.

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

Open in Gitpod

@github-actions
Copy link
Copy Markdown

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

PR summary 3bd2603b81

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Rel
+ Rel.exists
+ Rel.forall
+ Rel.left_mem
+ Rel.right_mem
+ Rel.symm
+ Rel.trans
+ empty_not_mem
+ eq_of_mem_inter
+ eq_of_mem_of_mem
+ instance (P : Partition u) : IsTrans α P.Rel
+ instance (P : Partition u) : Std.Symm P.Rel
+ mem_iff_exists
+ mem_iff_unique
+ nonempty_of_mem
+ rel_comm
+ rel_le_iff_le
+ rel_rfl_iff
+ rel_symmetric
+ sUnion_eq
+ subset_of_mem
+ subset_sUnion_and_mem_iff_mem
+ subset_sUnion_iff_mem

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

@github-actions github-actions bot added the t-order Order theory label Mar 22, 2026
This was referenced Mar 22, 2026
Open
Open
@mathlib-dependent-issues mathlib-dependent-issues bot added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Mar 22, 2026
@mathlib-dependent-issues
Copy link
Copy Markdown

mathlib-dependent-issues bot commented Mar 26, 2026

This PR/issue depends on:

@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 Mar 27, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Mar 27, 2026

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 Apr 1, 2026
@Jun2M Jun2M requested a review from YaelDillies April 1, 2026 20:35
YaelDillies
YaelDillies approved these changes Apr 3, 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 delegate

Mathlib/Order/Partition/Basic.lean
lemma nonempty_of_mem (ht : t ∈ P) : t.Nonempty :=
notMem_singleton_empty.1 <| P.ne_bot_of_mem ht

lemma empty_not_mem : ∅ ∉ P := P.bot_notMem
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies Apr 3, 2026

Choose a reason for hiding this comment

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

Suggested change
lemma empty_not_mem : ∅ ∉ P := P.bot_notMem
lemma empty_notMem : ∅ ∉ P := P.bot_notMem

is the convention now

@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 3, 2026

🚀 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 Apr 3, 2026
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

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-order Order theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@Jun2M @YaelDillies