Theorem Set.insert_Ioc_pred_right_eq_Ioc

Modification history

2026-09-03 14:21
Mathlib/Order/Interval/Set/SuccPred.lean
chore(Order/Interval/Set/SuccPred): use `to_dual` (#43366) …
Deleted Set.insert_Ioc_pred_right_eq_IocView on Github →
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_Ioc_pred_right_eq_IocView on Github →