Commit 2026-05-01 14:40 765d2232

View on Github →

chore(Order/SuccPred/Basic): use to_dual more (#38653)

Estimated changes

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

deleted theorem csInf_le

deleted theorem csInf_le_of_le

deleted theorem le_csInf

Modified Mathlib/Order/SuccPred/Basic.lean

deleted theorem Order.Icc_pred_left

deleted theorem Order.Ici_pred

deleted theorem Order.Ico_pred_left

deleted theorem Order.Ico_pred_right_eq_insert

deleted theorem Order.Ioc_pred_left

deleted theorem Order.Ioc_pred_left_of_not_isMin

deleted theorem Order.Ioi_pred_eq_insert

deleted theorem Order.Ioi_pred_eq_insert_of_not_isMin

deleted theorem Order.Ioo_eq_empty_iff_pred_le

deleted theorem Order.Ioo_pred_left

deleted theorem Order.Ioo_pred_left_of_not_isMin

deleted theorem Order.Ioo_pred_right_eq_insert

deleted theorem Order.not_isMax_pred

deleted theorem Order.pred_eq_csSup

deleted theorem Order.pred_eq_iSup

deleted theorem Order.pred_eq_sSup

deleted theorem Order.pred_succ

deleted theorem Order.pred_succ_of_not_isMax

deleted theorem Order.succ_pred_iterate_of_not_isMin

deleted theorem WithBot.orderSucc_bot

deleted theorem WithBot.orderSucc_coe

deleted theorem WithBot.pred_coe

deleted theorem WithBot.pred_coe_of_isMin

deleted theorem WithBot.pred_coe_of_not_isMin

deleted theorem WithBot.succ_unbot

modified theorem WithTop.orderPred_coe

modified theorem WithTop.orderPred_top