Theorem Partition.existsUnique_of_mem_le

Modification history

2026-04-14 15:28

Mathlib/Order/Partition/Basic.lean

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

Modified Partition.existsUnique_of_mem_le View on Github →

2026-03-26 22:21

Mathlib/Order/Partition/Basic.lean

feat(Order/Partition): add refinement order (#36574) …

Added Partition.existsUnique_of_mem_le View on Github →