Theorem Finset.insert_Icc_succ_left_eq_Icc

Modification history

2025-03-04 16:27

Mathlib/Order/Interval/Finset/SuccPred.lean

feat: `insert a (Icc (a + 1) b) = Icc a b` (#22559)

Added Finset.insert_Icc_succ_left_eq_Icc View on Github →