Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-04 16:21 21082848

View on Github →

refactor(order/succ_order/basic): Use is_min/is_max (#12597) Reformulate the succ a ≤ a and a ≤ pred a conditions to use is_max and is_min. This simplifies the proofs. Change namespaces from succ_order and pred_order to order. Lemma renames

Estimated changes

added theorem int.pred_eq_pred
modified theorem int.pred_iterate
added theorem int.succ_eq_succ
modified theorem int.succ_iterate
added theorem nat.pred_eq_pred
modified theorem nat.pred_iterate
added theorem nat.succ_eq_succ
modified theorem nat.succ_iterate
added theorem not_is_bot_iff_ne_bot
added theorem not_is_max_bot
added theorem not_is_max_iff_ne_top
added theorem not_is_min_iff_ne_bot
added theorem not_is_min_top
added theorem not_is_top_iff_ne_top
modified theorem with_top.not_top_le_coe
added theorem not_is_max_of_lt
added theorem not_is_min_of_lt
modified theorem covby.succ_eq
deleted theorem covby_iff_pred_eq
deleted theorem covby_iff_succ_eq
added theorem order.Ici_succ
added theorem order.Iic_pred
added theorem order.Iio_succ
added theorem order.Ioi_pred
added theorem order.bot_lt_succ
added theorem order.covby_succ
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_of_lt
added theorem order.le_succ
added theorem order.lt_succ
added theorem order.lt_succ_iff
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_eq_pred_iff
added theorem order.pred_eq_supr
added theorem order.pred_injective
added theorem order.pred_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_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_strict_mono
added theorem order.pred_succ
added def order.succ
added theorem order.succ_eq_infi
added theorem order.succ_eq_succ_iff
added theorem order.succ_injective
added theorem order.succ_le_iff
added theorem order.succ_le_of_lt
added theorem order.succ_le_succ
added theorem order.succ_le_succ_iff
added theorem order.succ_lt_succ_iff
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_strict_mono
added theorem order.succ_top
deleted theorem pred_order.le_pred_iff
deleted theorem pred_order.pred_bot
deleted theorem pred_order.pred_covby
deleted theorem pred_order.pred_eq_supr
deleted theorem pred_order.pred_injective
deleted theorem pred_order.pred_le_le_iff
deleted theorem pred_order.pred_le_pred
deleted theorem pred_order.pred_lt
deleted theorem pred_order.pred_lt_iff
deleted theorem pred_order.pred_lt_top
deleted theorem pred_order.pred_mono
deleted theorem pred_order.pred_ne_top
deleted theorem pred_succ
deleted theorem pred_succ_of_nonempty_Ioi
deleted theorem succ_order.bot_lt_succ
deleted theorem succ_order.covby_succ
deleted theorem succ_order.le_le_succ_iff
deleted theorem succ_order.lt_succ
deleted theorem succ_order.lt_succ_iff
deleted theorem succ_order.succ_eq_infi
deleted theorem succ_order.succ_injective
deleted theorem succ_order.succ_le_iff
deleted theorem succ_order.succ_le_succ
deleted theorem succ_order.succ_mono
deleted theorem succ_order.succ_ne_bot
deleted theorem succ_order.succ_top
deleted theorem succ_pred
deleted theorem succ_pred_of_nonempty_Iio