Commit 2026-04-05 15:16 1f7c79fe

View on Github →

feat(Order/Partition): add Rel, relation induced by partition on Set (#36991) 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.

Estimated changes

Modified Mathlib/Order/Partition/Basic.lean

added theorem Partition.Rel.exists

added theorem Partition.Rel.forall

added theorem Partition.Rel.left_mem

added theorem Partition.Rel.right_mem

added theorem Partition.Rel.symm

added theorem Partition.Rel.trans

added def Partition.Rel

added theorem Partition.empty_notMem

added theorem Partition.eq_of_mem_inter

added theorem Partition.eq_of_mem_of_mem

added theorem Partition.mem_iff_exists

added theorem Partition.mem_iff_unique

added theorem Partition.nonempty_of_mem

added theorem Partition.rel_comm

added theorem Partition.rel_le_iff_le

added theorem Partition.rel_rfl_iff

added theorem Partition.subset_of_mem

added theorem Partition.subset_sUnion_and_mem_iff_mem

added theorem Partition.subset_sUnion_iff_mem