Commit 2025-05-14 10:52 f55ac5ea

View on Github →

refactor: spell results using Minimal/MinimalFor (#23487) And move all the lemmas about existence of minimal/maximal elements in finite sets to a new file Order.Preorder.Finite. From Toric Moves:

  • Finite.exists_minimal_le -> Finite.exists_le_minimal

Estimated changes

deleted theorem Finset.exists_maximal
deleted theorem Finset.exists_minimal
deleted theorem Finite.exists_le_maximal
deleted theorem Finite.exists_minimal_le
deleted theorem Finset.exists_le_maximal
deleted theorem Finset.exists_minimal_le
deleted theorem Set.finite_isBot
deleted theorem Set.finite_isTop
added theorem maximalFor_eq_iff
added theorem maximalFor_id
added theorem minimalFor_eq_iff
added theorem minimalFor_id
added theorem Finset.exists_maximal
added theorem Finset.exists_minimal
added theorem Set.finite_isBot
added theorem Set.finite_isTop