Theorem Finset.insert_Icc_eq_Icc_sub_one_left

Modification history

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