Commit 2024-10-12 14:24 90f1b4da

View on Github →

chore(Order): move more defs to Defs (#17677)

Estimated changes

Modified Mathlib/Data/Fintype/Order.lean

Modified Mathlib/Order/CompleteLattice/Finset.lean

Modified Mathlib/Order/Defs.lean

added theorem Maximal.le_of_ge

added theorem Maximal.prop

added def Maximal

added theorem Minimal.le_of_le

added theorem Minimal.prop

added def Minimal

Modified Mathlib/Order/Filter/AtTopBot.lean

Modified Mathlib/Order/Minimal.lean

deleted theorem Maximal.le_of_ge

deleted theorem Maximal.prop

deleted def Maximal

deleted theorem Minimal.le_of_le

deleted theorem Minimal.prop

deleted def Minimal