Theorem Fintype.exists_disjointed_le

Modification history

2025-03-03 14:53
Mathlib/Order/Disjointed.lean
feat(Topology/Separation): coverings by disjoint clopens (#21079) …
Modified Fintype.exists_disjointed_leView on Github →
2025-01-21 20:44
Mathlib/Order/Disjointed.lean
refactor(Order/Disjointed): allow arbitrary partial orders as domain (#20545)
Added Fintype.exists_disjointed_leView on Github →