Theorem Set.insert_Ico_succ_left_eq_Ico

Modification history

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