Documentation

Mathlib.Data.List.Range

Ranges of naturals as lists #

This file shows basic results about List.iota, List.range, List.range' and defines List.finRange. finRange n is the list of elements of Fin n. iota n = [n, n - 1, ..., 1] and range n = [0, ..., n - 1] are basic list constructions used for tactics. range' a b = [a, ..., a + b - 1] is there to help prove properties about them. Actual maths should use List.Ico instead.

@[simp]
theorem List.range'_one {s : } {step : } :
List.range' s 1 step = [s]
theorem List.pairwise_lt_range' (s : ) (n : ) (step : optParam 1) :
autoParam (0 < step) _auto✝List.Pairwise (fun (x x_1 : ) => x < x_1) (List.range' s n step)
theorem List.nodup_range' (s : ) (n : ) (step : optParam 1) (h : autoParam (0 < step) _auto✝) :
@[simp]
theorem List.nthLe_range' {n : } {m : } {step : } (i : ) (H : i < List.length (List.range' n m step)) :
List.nthLe (List.range' n m step) i H = n + step * i
theorem List.nthLe_range'_1 {n : } {m : } (i : ) (H : i < List.length (List.range' n m)) :
List.nthLe (List.range' n m) i H = n + i
theorem List.pairwise_lt_range (n : ) :
List.Pairwise (fun (x x_1 : ) => x < x_1) (List.range n)
theorem List.pairwise_le_range (n : ) :
List.Pairwise (fun (x x_1 : ) => x x_1) (List.range n)
theorem List.chain'_range_succ (r : Prop) (n : ) :
List.Chain' r (List.range (Nat.succ n)) m < n, r m (Nat.succ m)
theorem List.chain_range_succ (r : Prop) (n : ) (a : ) :
List.Chain r a (List.range (Nat.succ n)) r a 0 m < n, r m (Nat.succ m)
theorem List.pairwise_gt_iota (n : ) :
List.Pairwise (fun (x x_1 : ) => x > x_1) (List.iota n)
def List.finRange (n : ) :
List (Fin n)

All elements of Fin n, from 0 to n-1. The corresponding finset is Finset.univ.

Equations
Instances For
    @[simp]
    theorem List.mem_finRange {n : } (a : Fin n) :
    @[simp]
    theorem List.finRange_eq_nil {n : } :
    List.finRange n = [] n = 0
    theorem List.pairwise_lt_finRange (n : ) :
    List.Pairwise (fun (x x_1 : Fin n) => x < x_1) (List.finRange n)
    theorem List.pairwise_le_finRange (n : ) :
    List.Pairwise (fun (x x_1 : Fin n) => x x_1) (List.finRange n)
    theorem List.sum_range_succ {α : Type u} [AddMonoid α] (f : α) (n : ) :
    theorem List.prod_range_succ {α : Type u} [Monoid α] (f : α) (n : ) :
    theorem List.sum_range_succ' {α : Type u} [AddMonoid α] (f : α) (n : ) :
    List.sum (List.map f (List.range (Nat.succ n))) = f 0 + List.sum (List.map (fun (i : ) => f (Nat.succ i)) (List.range n))

    A variant of sum_range_succ which pulls off the first term in the sum rather than the last.

    theorem List.prod_range_succ' {α : Type u} [Monoid α] (f : α) (n : ) :
    List.prod (List.map f (List.range (Nat.succ n))) = f 0 * List.prod (List.map (fun (i : ) => f (Nat.succ i)) (List.range n))

    A variant of prod_range_succ which pulls off the first term in the product rather than the last.

    @[simp]
    @[simp]
    theorem List.unzip_enumFrom_eq_prod {α : Type u} (l : List α) {n : } :
    @[simp]
    theorem List.nthLe_range {n : } (i : ) (H : i < List.length (List.range n)) :
    @[simp]
    theorem List.get_finRange {n : } {i : } (h : i < List.length (List.finRange n)) :
    List.get (List.finRange n) { val := i, isLt := h } = { val := i, isLt := }
    @[simp]
    @[simp]
    theorem List.nthLe_finRange {n : } {i : } (h : i < List.length (List.finRange n)) :
    List.nthLe (List.finRange n) i h = { val := i, isLt := }
    @[simp]
    theorem List.indexOf_finRange {k : } (i : Fin k) :

    From l : List, construct l.ranges : List (List ℕ) such that l.ranges.map List.length = l and l.ranges.join = range l.sum

    • Example: [1,2,3].ranges = [[0],[1,2],[3,4,5]]
    Equations
    Instances For
      theorem List.ranges_disjoint (l : List ) :
      List.Pairwise List.Disjoint (List.ranges l)

      The members of l.ranges are pairwise disjoint

      theorem List.ranges_length (l : List ) :
      List.map List.length (List.ranges l) = l

      The lengths of the members of l.ranges are those given by l

      theorem List.mem_mem_ranges_iff_lt_sum (l : List ) {n : } :
      (∃ s ∈ List.ranges l, n s) n < List.sum l

      Any entry of any member of l.ranges is strictly smaller than l.sum

      theorem List.ranges_nodup {l : List } {s : List } (hs : s List.ranges l) :

      The members of l.ranges have no duplicate