Theorem Finset.Ico_succ_right_eq_Icc_of_not_isMax

Modification history

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