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 : } :
@[simp]
theorem Finset.coe_range (n : ) :
@[simp]

Alias of the reverse direction of Finset.range_subset.

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

Alias of the reverse direction of Finset.nonempty_range_iff.

theorem Finset.nonempty_range_succ {n : } :
(Finset.range (n + 1)).Nonempty
theorem Finset.range_nontrivial {n : } (hn : 1 < n) :
(Finset.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,