Theorem Set.insert_Icc_pred_right_eq_Icc

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_Icc_pred_right_eq_IccView on Github →
2025-03-04 16:27
Mathlib/Order/Interval/Set/SuccPred.lean
feat: `insert a (Icc (a + 1) b) = Icc a b` (#22559)
Added Set.insert_Icc_pred_right_eq_IccView on Github →