Documentation

Mathlib.Data.Finset.Range

Finite sets made of a range of elements. #

Main declarations #

Finset constructions #

Tags #

finite sets, finset

range #

range n is the set of natural numbers less than n.

Equations
@[simp]
@[simp]
theorem Finset.mem_range {n m : } :
m range n m < n
@[simp]
theorem Finset.coe_range (n : ) :
(range n) = Set.Iio n
@[simp]
@[simp]
theorem Finset.range_add_one {n : } :
range (n + 1) = insert n (range n)
@[simp]
theorem Finset.range_subset {n m : } :

Alias of the reverse direction of Finset.range_subset.

theorem Finset.mem_range_le {n x : } (hx : x range n) :
x n
theorem Finset.mem_range_sub_ne_zero {n x : } (hx : x range n) :
n - x 0
@[simp]
theorem Finset.Aesop.range_nonempty {n : } :
n 0(range n).Nonempty

Alias of the reverse direction of Finset.nonempty_range_iff.

@[simp]
theorem Finset.range_nontrivial {n : } (hn : 1 < n) :

Equivalence between the set of natural numbers which are ≥ k and , given by n → n - k.

Equations
@[simp]
theorem coe_notMemRangeEquiv (k : ) :
(notMemRangeEquiv k) = fun (i : { n : // nMultiset.range k }) => i - k
@[simp]
theorem coe_notMemRangeEquiv_symm (k : ) :
(notMemRangeEquiv k).symm = fun (j : ) => j + k,