Commit 2026-03-26 22:21 c09416fb

View on Github →

feat(Order/Partition): add refinement order (#36574) 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.

Estimated changes

Modified Mathlib/Order/Partition/Basic.lean

modified theorem Partition.disjoint

added theorem Partition.eq_of_not_disjoint

added theorem Partition.eq_or_disjoint

added theorem Partition.existsUnique_of_mem_le

added theorem Partition.exists_le_of_mem_le

modified theorem Partition.ext

added theorem Partition.le_def

modified theorem Partition.mem_copy_iff

added theorem Partition.mem_removeBot

added theorem Partition.mem_top_iff

added theorem Partition.ne_bot_of_mem'

added theorem Partition.notMem_of_bot

added theorem Partition.parts_top

added theorem Partition.parts_top_subset

modified def Partition.partscopyEquiv

added theorem Partition.top_def