Commit 2025-03-04 16:27 e05e27cb

View on Github →

feat: insert a (Icc (a + 1) b) = Icc a b (#22559)

Estimated changes

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

added theorem Finset.insert_Icc_add_one_left_eq_Icc

added theorem Finset.insert_Icc_eq_Icc_add_one_right

added theorem Finset.insert_Icc_eq_Icc_sub_one_left

added theorem Finset.insert_Icc_sub_one_right_eq_Icc

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

added theorem Set.insert_Icc_add_one_left_eq_Icc

added theorem Set.insert_Icc_eq_Icc_add_one_right

added theorem Set.insert_Icc_eq_Icc_sub_one_left

added theorem Set.insert_Icc_sub_one_right_eq_Icc

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

added theorem Finset.insert_Icc_eq_Icc_pred_left

added theorem Finset.insert_Icc_eq_Icc_succ_right

added theorem Finset.insert_Icc_pred_right_eq_Icc

added theorem Finset.insert_Icc_succ_left_eq_Icc

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

added theorem Set.insert_Icc_eq_Icc_pred_left

added theorem Set.insert_Icc_eq_Icc_succ_right

added theorem Set.insert_Icc_pred_right_eq_Icc

added theorem Set.insert_Icc_succ_left_eq_Icc

Modified Mathlib/Order/SuccPred/Basic.lean

added theorem Order.le_iff_eq_or_le_pred

added theorem Order.le_iff_eq_or_succ_le