Theorem Set.insert_Ico_left_eq_Ico_sub_one_of_not_isMin

Modification history

2025-04-24 15:29
Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
feat: `insert (b + 1) (Ioc a b) = Ioc a (b + 1)` (#24037) …
Added Set.insert_Ico_left_eq_Ico_sub_one_of_not_isMinView on Github →