Theorem Nat.Icc_insert_succ_left

Modification history

2025-12-17 19:48
Mathlib/Order/Interval/Finset/Nat.lean
chore: remove March and April 2025 deprecated declarations (#32990) …
Deleted Nat.Icc_insert_succ_leftView on Github →
2024-07-20 10:12
Mathlib/Order/Interval/Finset/Nat.lean
feat(Order/Interval/Finset/Nat): `Icc_insert_succ_left`, `Icc_insert_succ_right` (#14838) …
Added Nat.Icc_insert_succ_leftView on Github →