Theorem Set.Icc_add_one_sub_one_eq_Ioo

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_add_one_sub_one_eq_Ioo View on Github →