Theorem DirectedOn.minimal_iff_isLeast

Modification history

2026-01-27 18:36
Mathlib/Order/Bounds/Basic.lean
feat(Order/Minimal): Minimal is equivalent to IsLeast if LE is total (#34388) …
Added DirectedOn.minimal_iff_isLeastView on Github →