Commit 2025-05-14 13:17 02065d27

View on Github →

feat: minimal elements exist in well-founded orders (#24766) From Toric

Estimated changes

Modified Mathlib/Order/Minimal.lean

added theorem exists_maximalFor_of_wellFoundedGT

added theorem exists_maximal_ge_of_wellFoundedGT

added theorem exists_maximal_of_wellFoundedGT

added theorem exists_minimalFor_of_wellFoundedLT

added theorem exists_minimal_le_of_wellFoundedLT

added theorem exists_minimal_of_wellFoundedLT