Commit 2024-07-16 23:35 d5307c03

View on Github →

feat(Order): Galois connection between pred and succ (#13505) This was a longstanding TODO. Kudos to Kevin for putting the pieces together!

Estimated changes

Modified Mathlib/Order/Cover.lean

Modified Mathlib/Order/SuccPred/Basic.lean

deleted theorem CovBy.pred_eq

deleted theorem CovBy.succ_eq

added theorem Order.gc_pred_succ

added theorem Order.le_succ_of_wcovBy

added theorem Order.le_succ_pred

added theorem Order.pred_eq_of_covBy

added theorem Order.pred_le_iff_le_succ

added theorem Order.pred_le_of_wcovBy

added theorem Order.pred_succ_le

added theorem Order.succ_eq_of_covBy

deleted theorem WCovBy.le_succ

deleted theorem WCovBy.pred_le