Theorem Set.Icc_sub_one_right_eq_Ico_of_not_isMin

Modification history

2025-02-26 15:28
Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
feat: interaction of finite intervals and succ/pred (#22290)
Added Set.Icc_sub_one_right_eq_Ico_of_not_isMinView on Github →