Theorem Finset.nonempty_range_add_one

Modification history

2025-09-11 00:00
Mathlib/Data/Finset/Range.lean
chore(Data/Finset): deprecate `range_succ`; rename `range_subset` to `range_subset_range` (#29509) …
Added Finset.nonempty_range_add_oneView on Github →