Commit 2026-01-27 18:36 4033a645

View on Github →

feat(Order/Minimal): Minimal is equivalent to IsLeast if LE is total (#34388) If a set is DirectedOn, then Minimal(and Maximal) is equivalent to IsLeast(and IsGreatest). If the type has a total order, every set is DirectedOn and therefore the proof of DirectedOn is not needed.

Estimated changes

Modified Mathlib/Order/Bounds/Basic.lean

added theorem DirectedOn.le_of_maximal

added theorem DirectedOn.le_of_minimal

added theorem DirectedOn.maximal_iff_isGreatest

added theorem DirectedOn.minimal_iff_isLeast

added theorem maximal_iff_isGreatest

added theorem minimal_iff_isLeast

Modified Mathlib/Order/Directed.lean

added theorem Std.Total.directedOn

Modified Mathlib/Order/Minimal.lean

added theorem Maximal.le

added theorem MaximalFor.le

added theorem MaximalFor.not_gt

added theorem MaximalFor.not_prop_of_gt

added theorem Minimal.le

added theorem MinimalFor.le

added theorem MinimalFor.not_lt

added theorem MinimalFor.not_prop_of_lt

added theorem maximalFor_iff_forall_gt

added theorem minimalFor_iff_forall_lt