Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-19 08:07 9202b6d1

View on Github →

feat(order/succ_pred/basic): Intervals and succ/pred (#13486) Relate order.succ, order.pred and set.Ixx.

Estimated changes

deleted theorem set.insert_inter
modified theorem set.insert_inter_of_mem
modified theorem set.insert_inter_of_not_mem
added theorem set.Ico_insert_right
added theorem set.Iic_inter_Ici
added theorem set.Iic_inter_Ioi
added theorem set.Iio_insert
added theorem set.Iio_inter_Ici
added theorem set.Iio_inter_Ioi
added theorem set.Ioc_insert_left
added theorem set.Ioi_insert
added theorem set.Ioo_insert_left
added theorem set.Ioo_insert_right
added theorem and_and_distrib_left
added theorem and_and_distrib_right
added theorem or_or_distrib_left
added theorem or_or_distrib_right
added theorem order.Icc_pred_left
added theorem order.Icc_pred_right
added theorem order.Icc_succ_left
added theorem order.Icc_succ_right
added theorem order.Ici_pred
modified theorem order.Ici_succ
added theorem order.Ico_pred_left
added theorem order.Ico_succ_left
added theorem order.Ico_succ_right
modified theorem order.Iic_pred
added theorem order.Iic_succ
modified theorem order.Iio_succ
added theorem order.Ioc_pred_left
added theorem order.Ioc_pred_right
added theorem order.Ioc_succ_right
modified theorem order.Ioi_pred
added theorem order.Ioo_pred_left
added theorem order.Ioo_succ_right