Finite sets made of a range of elements. #
Main declarations #
Finset constructions #
Finset.range
: For anyn : ℕ
,range n
is equal to{0, 1, ... , n - 1} ⊆ ℕ
. This convention is consistent with other languages and normalizescard (range n) = n
. Beware,n
is not inrange n
.
Tags #
finite sets, finset
range #
@[deprecated Finset.notMem_range_self (since := "2025-05-23")]
Alias of Finset.notMem_range_self
.
Alias of the reverse direction of Finset.range_subset
.
Alias of the reverse direction of Finset.nonempty_range_iff
.
@[simp]
@[simp]