Theorem Finset.insert_Ioc_sub_one_right_eq_Ioc

Modification history

2025-04-05 16:03
Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
feat: `insert b (Ico a b) = Ico a (b + 1)` (#23630) …
Added Finset.insert_Ioc_sub_one_right_eq_IocView on Github →