Commit 2025-02-14 03:34 449e7291

View on Github →

feat(Order/Partition/Basic): partitions of lattice elements (#21428) This provides a version of Finpartition where the partition can have infinitely many parts.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Partition/Basic.lean

added def Partition.Simps.coe

added theorem Partition.bot_lt_of_mem

added theorem Partition.bot_not_mem

added theorem Partition.coe_parts

added theorem Partition.disjoint

added theorem Partition.ext

added theorem Partition.iSup_eq

added theorem Partition.le_of_mem

added theorem Partition.mem_copy_iff

added theorem Partition.ne_bot_of_mem

added theorem Partition.pairwiseDisjoint

added theorem Partition.parts_nonempty

added def Partition.partscopyEquiv

added def Partition.removeBot

added theorem Partition.sSupIndep

added theorem Partition.sSup_eq

added structure Partition