Theorem Finset.insert_Ico_right_eq_Ico_succ_right_of_not_isMax

Modification history

2025-04-24 15:29
Mathlib/Order/Interval/Finset/SuccPred.lean
feat: `insert (b + 1) (Ioc a b) = Ioc a (b + 1)` (#24037) …
Deleted Finset.insert_Ico_right_eq_Ico_succ_right_of_not_isMaxView on Github →
2025-04-05 16:03
Mathlib/Order/Interval/Finset/SuccPred.lean
feat: `insert b (Ico a b) = Ico a (b + 1)` (#23630) …
Added Finset.insert_Ico_right_eq_Ico_succ_right_of_not_isMaxView on Github →