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
    Instances For
      @[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)
      @[deprecated Finset.notMem_range_self (since := "2025-05-23")]
      theorem Finset.not_mem_range_self {n : } :
      nrange n

      Alias of Finset.notMem_range_self.

      @[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
        Instances For
          @[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,