Commit 2025-04-24 15:29 9062fa84

View on Github →

feat: insert (b + 1) (Ioc a b) = Ioc a (b + 1) (#24037) And shorten recently introduced names for consistency

Estimated changes

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

deleted theorem Finset.insert_Icc_eq_Icc_add_one_right

deleted theorem Finset.insert_Icc_eq_Icc_sub_one_left

added theorem Finset.insert_Icc_left_eq_Icc_sub_one

added theorem Finset.insert_Icc_right_eq_Icc_add_one

added theorem Finset.insert_Ico_left_eq_Ico_sub_one

added theorem Finset.insert_Ico_left_eq_Ico_sub_one_of_not_isMin

added theorem Finset.insert_Ico_right_eq_Ico_add_one

added theorem Finset.insert_Ico_right_eq_Ico_add_one_of_not_isMax

deleted theorem Finset.insert_Ico_right_eq_Ico_add_one_right

deleted theorem Finset.insert_Ico_right_eq_Ico_add_one_right_of_not_isMax

added theorem Finset.insert_Ico_sub_one_right_eq_Ico

added theorem Finset.insert_Ioc_add_one_left_eq_Ioc

added theorem Finset.insert_Ioc_left_eq_Ioc_sub_one

deleted theorem Finset.insert_Ioc_left_eq_Ioc_sub_one_left

deleted theorem Finset.insert_Ioc_left_eq_Ioc_sub_one_left_of_not_isMin

added theorem Finset.insert_Ioc_left_eq_Ioc_sub_one_of_not_isMin

added theorem Finset.insert_Ioc_right_eq_Ioc_add_one

added theorem Finset.insert_Ioc_right_eq_Ioc_add_one_of_not_isMax

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

deleted theorem Set.insert_Icc_eq_Icc_add_one_right

deleted theorem Set.insert_Icc_eq_Icc_sub_one_left

added theorem Set.insert_Icc_left_eq_Icc_sub_one

added theorem Set.insert_Icc_right_eq_Icc_add_one

added theorem Set.insert_Ico_left_eq_Ico_sub_one

added theorem Set.insert_Ico_left_eq_Ico_sub_one_of_not_isMin

added theorem Set.insert_Ico_right_eq_Ico_add_one

added theorem Set.insert_Ico_right_eq_Ico_add_one_of_not_isMax

deleted theorem Set.insert_Ico_right_eq_Ico_add_one_right

deleted theorem Set.insert_Ico_right_eq_Ico_add_one_right_of_not_isMax

added theorem Set.insert_Ico_sub_one_right_eq_Ico

added theorem Set.insert_Ioc_add_one_left_eq_Ioc

added theorem Set.insert_Ioc_left_eq_Ioc_sub_one

deleted theorem Set.insert_Ioc_left_eq_Ioc_sub_one_left

deleted theorem Set.insert_Ioc_left_eq_Ioc_sub_one_left_of_not_isMin

added theorem Set.insert_Ioc_left_eq_Ioc_sub_one_of_not_isMin

added theorem Set.insert_Ioc_right_eq_Ioc_add_one

added theorem Set.insert_Ioc_right_eq_Ioc_add_one_of_not_isMax

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

deleted theorem Finset.insert_Icc_eq_Icc_pred_left

deleted theorem Finset.insert_Icc_eq_Icc_succ_right

added theorem Finset.insert_Icc_left_eq_Icc_pred

added theorem Finset.insert_Icc_right_eq_Icc_succ

added theorem Finset.insert_Ico_left_eq_Ico_pred

added theorem Finset.insert_Ico_left_eq_Ico_pred_of_not_isMin

added theorem Finset.insert_Ico_pred_right_eq_Ico

added theorem Finset.insert_Ico_right_eq_Ico_succ

added theorem Finset.insert_Ico_right_eq_Ico_succ_of_not_isMax

deleted theorem Finset.insert_Ico_right_eq_Ico_succ_right

deleted theorem Finset.insert_Ico_right_eq_Ico_succ_right_of_not_isMax

added theorem Finset.insert_Ioc_left_eq_Ioc_pred

deleted theorem Finset.insert_Ioc_left_eq_Ioc_pred_left

deleted theorem Finset.insert_Ioc_left_eq_Ioc_pred_left_of_not_isMin

added theorem Finset.insert_Ioc_left_eq_Ioc_pred_of_not_isMin

added theorem Finset.insert_Ioc_right_eq_Ioc_succ

added theorem Finset.insert_Ioc_right_eq_Ioc_succ_of_not_isMax

added theorem Finset.insert_Ioc_succ_left_eq_Ioc

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

deleted theorem Set.insert_Icc_eq_Icc_pred_left

deleted theorem Set.insert_Icc_eq_Icc_succ_right

added theorem Set.insert_Icc_left_eq_Icc_pred

added theorem Set.insert_Icc_right_eq_Icc_succ

added theorem Set.insert_Ico_left_eq_Ico_pred

added theorem Set.insert_Ico_left_eq_Ico_pred_of_not_isMin

added theorem Set.insert_Ico_pred_right_eq_Ico

added theorem Set.insert_Ico_right_eq_Ico_succ

added theorem Set.insert_Ico_right_eq_Ico_succ_of_not_isMax

deleted theorem Set.insert_Ico_right_eq_Ico_succ_right

deleted theorem Set.insert_Ico_right_eq_Ico_succ_right_of_not_isMax

added theorem Set.insert_Ioc_left_eq_Ioc_pred

deleted theorem Set.insert_Ioc_left_eq_Ioc_pred_left

deleted theorem Set.insert_Ioc_left_eq_Ioc_pred_left_of_not_isMin

added theorem Set.insert_Ioc_left_eq_Ioc_pred_of_not_isMin

added theorem Set.insert_Ioc_right_eq_Ioc_succ

added theorem Set.insert_Ioc_right_eq_Ioc_succ_of_not_isMax

added theorem Set.insert_Ioc_succ_left_eq_Ioc