Theorem Finset.Icc_sub_one_right_eq_Ico

Modification history

2025-02-26 15:28

Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean

feat: interaction of finite intervals and succ/pred (#22290)

Added Finset.Icc_sub_one_right_eq_Ico View on Github →