Commit 2023-01-01 19:51 a6184c4b

View on Github →

feat: port Order.SuccPred.Basic (#1233) Port of order.succ_pred.basic

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/RelClasses.lean

Created Mathlib/Order/SuccPred/Basic.lean

added theorem LE.le.exists_pred_iterate

added theorem LE.le.exists_succ_iterate

added theorem Order.Covby.pred_eq

added theorem Order.Covby.succ_eq

added theorem Order.Icc_pred_left

added theorem Order.Icc_pred_right

added theorem Order.Icc_pred_right_of_not_isMin

added theorem Order.Icc_succ_left

added theorem Order.Icc_succ_left_of_not_isMax

added theorem Order.Icc_succ_right

added theorem Order.Ici_pred

added theorem Order.Ici_succ

added theorem Order.Ici_succ_of_not_isMax

added theorem Order.Ico_pred_left

added theorem Order.Ico_pred_right_eq_insert

added theorem Order.Ico_succ_left

added theorem Order.Ico_succ_left_of_not_isMax

added theorem Order.Ico_succ_right

added theorem Order.Ico_succ_right_eq_insert

added theorem Order.Ico_succ_right_eq_insert_of_not_isMax

added theorem Order.Ico_succ_right_of_not_isMax

added theorem Order.Iic_pred

added theorem Order.Iic_pred_of_not_isMin

added theorem Order.Iic_succ

added theorem Order.Iio_succ

added theorem Order.Iio_succ_eq_insert

added theorem Order.Iio_succ_eq_insert_of_not_isMax

added theorem Order.Iio_succ_of_not_isMax

added theorem Order.Ioc_pred_left

added theorem Order.Ioc_pred_left_of_not_isMin

added theorem Order.Ioc_pred_right

added theorem Order.Ioc_pred_right_of_not_isMin

added theorem Order.Ioc_succ_right

added theorem Order.Ioi_pred

added theorem Order.Ioi_pred_eq_insert

added theorem Order.Ioi_pred_eq_insert_of_not_isMin

added theorem Order.Ioi_pred_of_not_isMin

added theorem Order.Ioo_pred_left

added theorem Order.Ioo_pred_left_of_not_isMin

added theorem Order.Ioo_pred_right_eq_insert

added theorem Order.Ioo_succ_right

added theorem Order.Ioo_succ_right_eq_insert

added theorem Order.Ioo_succ_right_eq_insert_of_not_isMax

added theorem Order.Ioo_succ_right_of_not_isMax

added theorem Order.Wcovby.le_succ

added theorem Order.Wcovby.pred_le

added theorem Order.bot_lt_succ

added theorem Order.covby_succ

added theorem Order.covby_succ_of_not_isMax

added theorem Order.isMax_iterate_succ_of_eq_of_lt

added theorem Order.isMax_iterate_succ_of_eq_of_ne

added theorem Order.isMin_iterate_pred_of_eq_of_lt

added theorem Order.isMin_iterate_pred_of_eq_of_ne

added theorem Order.le_le_succ_iff

added theorem Order.le_of_lt_succ

added theorem Order.le_of_pred_lt

added theorem Order.le_pred_iff

added theorem Order.le_pred_iff_eq_bot

added theorem Order.le_pred_iff_isMin

added theorem Order.le_pred_iff_of_not_isMin

added theorem Order.le_pred_of_lt

added theorem Order.le_succ

added theorem Order.le_succ_bot_iff

added theorem Order.le_succ_iff_eq_or_le

added theorem Order.le_succ_iterate

added theorem Order.lt_succ

added theorem Order.lt_succ_bot_iff

added theorem Order.lt_succ_iff

added theorem Order.lt_succ_iff_eq_or_lt

added theorem Order.lt_succ_iff_eq_or_lt_of_not_isMax

added theorem Order.lt_succ_iff_ne_top

added theorem Order.lt_succ_iff_not_isMax

added theorem Order.lt_succ_iff_of_not_isMax

added theorem Order.max_of_succ_le

added theorem Order.min_of_le_pred

added def Order.pred

added theorem Order.pred_bot

added theorem Order.pred_covby

added theorem Order.pred_covby_of_not_isMin

added theorem Order.pred_eq_iff_covby

added theorem Order.pred_eq_iff_isMin

added theorem Order.pred_eq_pred_iff

added theorem Order.pred_eq_supᵢ

added theorem Order.pred_injective

added theorem Order.pred_iterate_le

added theorem Order.pred_le

added theorem Order.pred_le_iff_eq_or_le

added theorem Order.pred_le_le_iff

added theorem Order.pred_le_pred

added theorem Order.pred_le_pred_iff

added theorem Order.pred_lt

added theorem Order.pred_lt_iff

added theorem Order.pred_lt_iff_eq_or_lt

added theorem Order.pred_lt_iff_eq_or_lt_of_not_isMin

added theorem Order.pred_lt_iff_ne_bot

added theorem Order.pred_lt_iff_not_isMin

added theorem Order.pred_lt_iff_of_not_isMin

added theorem Order.pred_lt_pred_iff

added theorem Order.pred_lt_top

added theorem Order.pred_mono

added theorem Order.pred_ne_pred_iff

added theorem Order.pred_ne_top

added theorem Order.pred_strictMono

added theorem Order.pred_succ

added theorem Order.pred_succ_iterate_of_not_isMax

added theorem Order.pred_succ_of_not_isMax

added theorem Order.pred_top_le_iff

added theorem Order.pred_top_lt_iff

added theorem Order.pred_wcovby

added def Order.succ

added theorem Order.succ_eq_iff_covby

added theorem Order.succ_eq_iff_isMax

added theorem Order.succ_eq_infᵢ

added theorem Order.succ_eq_succ_iff

added theorem Order.succ_eq_succ_iff_of_not_isMax

added theorem Order.succ_injective

added theorem Order.succ_le_iff

added theorem Order.succ_le_iff_eq_top

added theorem Order.succ_le_iff_isMax

added theorem Order.succ_le_iff_of_not_isMax

added theorem Order.succ_le_of_lt

added theorem Order.succ_le_succ

added theorem Order.succ_le_succ_iff

added theorem Order.succ_le_succ_iff_of_not_isMax

added theorem Order.succ_lt_succ_iff

added theorem Order.succ_lt_succ_iff_of_not_isMax

added theorem Order.succ_mono

added theorem Order.succ_ne_bot

added theorem Order.succ_ne_succ_iff

added theorem Order.succ_pred

added theorem Order.succ_pred_iterate_of_not_isMin

added theorem Order.succ_pred_of_not_isMin

added theorem Order.succ_strictMono

added theorem Order.succ_top

added theorem Order.wcovby_succ

added theorem Pred.rec

added theorem Pred.rec_iff

added theorem Pred.rec_linear

added theorem Pred.rec_top

added def PredOrder.ofCore

added def PredOrder.ofLePredIff

added def PredOrder.ofLePredIffOfPredLePred

added theorem Succ.rec

added theorem Succ.rec_bot

added theorem Succ.rec_iff

added theorem Succ.rec_linear

added def SuccOrder.ofCore

added def SuccOrder.ofSuccLeIff

added def SuccOrder.ofSuccLeIffOfLeLtSucc

added theorem WithBot.pred_coe

added theorem WithBot.pred_coe_bot

added theorem WithBot.pred_coe_of_ne_bot

added theorem WithBot.succ_bot

added theorem WithBot.succ_coe

added theorem WithTop.pred_coe

added theorem WithTop.pred_top

added theorem WithTop.succ_coe

added theorem WithTop.succ_coe_of_ne_top

added theorem WithTop.succ_coe_top

added theorem exists_pred_iterate_iff_le

added theorem exists_pred_iterate_or

added theorem exists_succ_iterate_iff_le

added theorem exists_succ_iterate_or