Commit 2025-02-26 15:28 ae7f5ae7

View on Github →

feat: interaction of finite intervals and succ/pred (#22290)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Intervals.lean

Renamed Mathlib/Algebra/Order/Interval/Finset.lean to Mathlib/Algebra/Order/Interval/Finset/Basic.lean

Created Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean

added theorem Finset.Icc_add_one_left_eq_Ioc

added theorem Finset.Icc_add_one_left_eq_Ioc_of_not_isMax

added theorem Finset.Icc_add_one_sub_one_eq_Ioo

added theorem Finset.Icc_sub_one_right_eq_Ico

added theorem Finset.Icc_sub_one_right_eq_Ico_of_not_isMin

added theorem Finset.Ici_add_one_eq_Ioi

added theorem Finset.Ici_add_one_eq_Ioi_of_not_isMax

added theorem Finset.Ico_add_one_add_one_eq_Ioc

added theorem Finset.Ico_add_one_add_one_eq_Ioc_of_not_isMax

added theorem Finset.Ico_add_one_left_eq_Ioo

added theorem Finset.Ico_add_one_right_eq_Icc

added theorem Finset.Ico_add_one_right_eq_Icc_of_not_isMax

added theorem Finset.Iic_sub_one_eq_Iio

added theorem Finset.Iic_sub_one_eq_Iio_of_not_isMin

added theorem Finset.Iio_add_one_eq_Iic

added theorem Finset.Iio_add_one_eq_Iic_of_not_isMax

added theorem Finset.Ioc_sub_one_left_eq_Icc

added theorem Finset.Ioc_sub_one_left_eq_Icc_of_not_isMin

added theorem Finset.Ioc_sub_one_right_eq_Ioo

added theorem Finset.Ioc_sub_one_sub_one_eq_Ico

added theorem Finset.Ioc_sub_one_sub_one_eq_Ico_of_not_isMin

added theorem Finset.Ioi_sub_one_eq_Ici

added theorem Finset.Ioi_sub_one_eq_Ici_of_not_isMin

added theorem Finset.Ioo_add_one_right_eq_Ioc

added theorem Finset.Ioo_add_one_right_eq_Ioc_of_not_isMax

added theorem Finset.Ioo_sub_one_left_eq_Ioc

added theorem Finset.Ioo_sub_one_left_eq_Ioc_of_not_isMin

Modified Mathlib/Algebra/Order/Interval/Multiset.lean

Created Mathlib/Algebra/Order/Interval/Set/SuccPred.lean

added theorem Set.Icc_add_one_left_eq_Ioc

added theorem Set.Icc_add_one_left_eq_Ioc_of_not_isMax

added theorem Set.Icc_add_one_sub_one_eq_Ioo

added theorem Set.Icc_sub_one_right_eq_Ico

added theorem Set.Icc_sub_one_right_eq_Ico_of_not_isMin

added theorem Set.Ici_add_one_eq_Ioi

added theorem Set.Ici_add_one_eq_Ioi_of_not_isMax

added theorem Set.Ico_add_one_add_one_eq_Ioc

added theorem Set.Ico_add_one_add_one_eq_Ioc_of_not_isMax

added theorem Set.Ico_add_one_left_eq_Ioo

added theorem Set.Ico_add_one_right_eq_Icc

added theorem Set.Ico_add_one_right_eq_Icc_of_not_isMax

added theorem Set.Iic_sub_one_eq_Iio

added theorem Set.Iic_sub_one_eq_Iio_of_not_isMin

added theorem Set.Iio_add_one_eq_Iic

added theorem Set.Iio_add_one_eq_Iic_of_not_isMax

added theorem Set.Ioc_sub_one_left_eq_Icc

added theorem Set.Ioc_sub_one_left_eq_Icc_of_not_isMin

added theorem Set.Ioc_sub_one_right_eq_Ioo

added theorem Set.Ioc_sub_one_sub_one_eq_Ico

added theorem Set.Ioc_sub_one_sub_one_eq_Ico_of_not_isMin

added theorem Set.Ioi_sub_one_eq_Ici

added theorem Set.Ioi_sub_one_eq_Ici_of_not_isMin

added theorem Set.Ioo_add_one_right_eq_Ioc

added theorem Set.Ioo_add_one_right_eq_Ioc_of_not_isMax

added theorem Set.Ioo_sub_one_left_eq_Ioc

added theorem Set.Ioo_sub_one_left_eq_Ioc_of_not_isMin

Modified Mathlib/Combinatorics/Additive/AP/Three/Defs.lean

Created Mathlib/Order/Interval/Finset/SuccPred.lean

added theorem Finset.Icc_pred_right_eq_Ico

added theorem Finset.Icc_pred_right_eq_Ico_of_not_isMin

added theorem Finset.Icc_succ_left_eq_Ioc

added theorem Finset.Icc_succ_left_eq_Ioc_of_not_isMax

added theorem Finset.Icc_succ_pred_eq_Ioo

added theorem Finset.Ici_succ_eq_Ioi

added theorem Finset.Ici_succ_eq_Ioi_of_not_isMax

added theorem Finset.Ico_succ_left_eq_Ioo

added theorem Finset.Ico_succ_right_eq_Icc

added theorem Finset.Ico_succ_right_eq_Icc_of_not_isMax

added theorem Finset.Ico_succ_succ_eq_Ioc

added theorem Finset.Ico_succ_succ_eq_Ioc_of_not_isMax

added theorem Finset.Iic_pred_eq_Iio

added theorem Finset.Iic_pred_eq_Iio_of_not_isMin

added theorem Finset.Iio_succ_eq_Iic

added theorem Finset.Iio_succ_eq_Iic_of_not_isMax

added theorem Finset.Ioc_pred_left_eq_Icc

added theorem Finset.Ioc_pred_left_eq_Icc_of_not_isMin

added theorem Finset.Ioc_pred_pred_eq_Ico

added theorem Finset.Ioc_pred_pred_eq_Ico_of_not_isMin

added theorem Finset.Ioc_pred_right_eq_Ioo

added theorem Finset.Ioi_pred_eq_Ici

added theorem Finset.Ioi_pred_eq_Ici_of_not_isMin

added theorem Finset.Ioo_pred_left_eq_Ioc

added theorem Finset.Ioo_pred_left_eq_Ioc_of_not_isMin

added theorem Finset.Ioo_succ_right_eq_Ioc

added theorem Finset.Ioo_succ_right_eq_Ioc_of_not_isMax

Created Mathlib/Order/Interval/Set/SuccPred.lean

added theorem Set.Icc_pred_right_eq_Ico

added theorem Set.Icc_pred_right_eq_Ico_of_not_isMin

added theorem Set.Icc_succ_left_eq_Ioc

added theorem Set.Icc_succ_left_eq_Ioc_of_not_isMax

added theorem Set.Icc_succ_pred_eq_Ioo

added theorem Set.Ici_succ_eq_Ioi

added theorem Set.Ici_succ_eq_Ioi_of_not_isMax

added theorem Set.Ico_succ_left_eq_Ioo

added theorem Set.Ico_succ_right_eq_Icc

added theorem Set.Ico_succ_right_eq_Icc_of_not_isMax

added theorem Set.Ico_succ_succ_eq_Ioc

added theorem Set.Ico_succ_succ_eq_Ioc_of_not_isMax

added theorem Set.Iic_pred_eq_Iio

added theorem Set.Iic_pred_eq_Iio_of_not_isMin

added theorem Set.Iio_succ_eq_Iic

added theorem Set.Iio_succ_eq_Iic_of_not_isMax

added theorem Set.Ioc_pred_left_eq_Icc

added theorem Set.Ioc_pred_left_eq_Icc_of_not_isMin

added theorem Set.Ioc_pred_pred_eq_Ico

added theorem Set.Ioc_pred_pred_eq_Ico_of_not_isMin

added theorem Set.Ioc_pred_right_eq_Ioo

added theorem Set.Ioi_pred_eq_Ici

added theorem Set.Ioi_pred_eq_Ici_of_not_isMin

added theorem Set.Ioo_pred_left_eq_Ioc

added theorem Set.Ioo_pred_left_eq_Ioc_of_not_isMin

added theorem Set.Ioo_succ_right_eq_Ioc

added theorem Set.Ioo_succ_right_eq_Ioc_of_not_isMax