Commit 2024-07-29 16:50 fdd94c07

View on Github →

feat(Order/Minimal): generalize PartialOrder to Preorder where possible (#15196) from the Carleson project.

Estimated changes

Modified Mathlib/Order/Minimal.lean

modified theorem IsAntichain.maximals_lowerClosure

modified theorem IsAntichain.minimals_upperClosure

modified theorem IsGreatest.maximals_eq

modified theorem IsGreatest.mem_maximals

modified theorem IsLeast.mem_minimals

modified theorem IsLeast.minimals_eq

modified theorem mem_maximals_iff_forall_lt_not_mem

modified theorem mem_minimals_iff_forall_lt_not_mem