Commit 2025-04-05 16:03 28f8afef

View on Github →

feat: insert b (Ico a b) = Ico a (b + 1) (#23630) and similar lemmas. Copied over from Order.Interval.Finset.Nat.

Estimated changes

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

added theorem Finset.insert_Ico_add_one_left_eq_Ico

added theorem Finset.insert_Ico_right_eq_Ico_add_one_right

added theorem Finset.insert_Ico_right_eq_Ico_add_one_right_of_not_isMax

added theorem Finset.insert_Ioc_left_eq_Ioc_sub_one_left

added theorem Finset.insert_Ioc_left_eq_Ioc_sub_one_left_of_not_isMin

added theorem Finset.insert_Ioc_sub_one_right_eq_Ioc

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

added theorem Set.insert_Ico_add_one_left_eq_Ico

added theorem Set.insert_Ico_right_eq_Ico_add_one_right

added theorem Set.insert_Ico_right_eq_Ico_add_one_right_of_not_isMax

added theorem Set.insert_Ioc_left_eq_Ioc_sub_one_left

added theorem Set.insert_Ioc_left_eq_Ioc_sub_one_left_of_not_isMin

added theorem Set.insert_Ioc_sub_one_right_eq_Ioc

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

added theorem Finset.insert_Ico_right_eq_Ico_succ_right

added theorem Finset.insert_Ico_right_eq_Ico_succ_right_of_not_isMax

added theorem Finset.insert_Ico_succ_left_eq_Ico

added theorem Finset.insert_Ioc_left_eq_Ioc_pred_left

added theorem Finset.insert_Ioc_left_eq_Ioc_pred_left_of_not_isMin

added theorem Finset.insert_Ioc_pred_right_eq_Ioc

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

added theorem Set.insert_Ico_right_eq_Ico_succ_right

added theorem Set.insert_Ico_right_eq_Ico_succ_right_of_not_isMax

added theorem Set.insert_Ico_succ_left_eq_Ico

added theorem Set.insert_Ioc_left_eq_Ioc_pred_left

added theorem Set.insert_Ioc_left_eq_Ioc_pred_left_of_not_isMin

added theorem Set.insert_Ioc_pred_right_eq_Ioc