Theorem DirectedOn.maximal_iff_isGreatest

Modification history

2026-08-10 08:17
Mathlib/Order/Bounds/Basic.lean
chore(Order/Bounds/Basic): add missing `to_dual` tags (#40040) …
Deleted DirectedOn.maximal_iff_isGreatestView on Github →
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.maximal_iff_isGreatestView on Github →