Theorem Set.Ioc_pred_pred_eq_Ico_of_not_isMin

Modification history

2026-09-03 14:21
Mathlib/Order/Interval/Set/SuccPred.lean
chore(Order/Interval/Set/SuccPred): use `to_dual` (#43366) …
Deleted Set.Ioc_pred_pred_eq_Ico_of_not_isMinView on Github →
2025-02-26 15:28
Mathlib/Order/Interval/Set/SuccPred.lean
feat: interaction of finite intervals and succ/pred (#22290)
Added Set.Ioc_pred_pred_eq_Ico_of_not_isMinView on Github →