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]
theorem Finset.range_val (n : ) :
@[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_one :
range 1 = {0}
theorem Finset.range_succ {n : } :
range n.succ = insert n (range n)
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_succ_iff {a b : } :
a range b.succ a b
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.nonempty_range_iff {n : } :
(range n).Nonempty n 0
theorem Finset.Aesop.range_nonempty {n : } :
n 0(range n).Nonempty

Alias of the reverse direction of Finset.nonempty_range_iff.

@[simp]
theorem Finset.nonempty_range_succ {n : } :
(range (n + 1)).Nonempty
theorem Finset.range_nontrivial {n : } (hn : 1 < n) :
(range n).Nontrivial
def notMemRangeEquiv (k : ) :
{ n : // nMultiset.range k }

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,