Documentation

Mathlib.Data.List.Sublists

sublists #

List.Sublists gives a list of all (not necessarily contiguous) sublists of a list.

This file contains basic results on this function.

sublists #

@[simp]
theorem List.sublists'_nil {α : Type u} :
[].sublists' = [[]]
@[simp]
theorem List.sublists'_singleton {α : Type u} (a : α) :
[a].sublists' = [[], [a]]
def List.sublists'Aux {α : Type u} (a : α) (r₁ : List (List α)) (r₂ : List (List α)) :
List (List α)

Auxiliary helper definition for sublists'

Equations
Instances For
    theorem List.sublists'Aux_eq_array_foldl {α : Type u} (a : α) (r₁ : List (List α)) (r₂ : List (List α)) :
    List.sublists'Aux a r₁ r₂ = (Array.foldl (fun (r : Array (List α)) (l : List α) => r.push (a :: l)) r₂.toArray r₁.toArray).toList
    theorem List.sublists'_eq_sublists'Aux {α : Type u} (l : List α) :
    l.sublists' = List.foldr (fun (a : α) (r : List (List α)) => List.sublists'Aux a r r) [[]] l
    theorem List.sublists'Aux_eq_map {α : Type u} (a : α) (r₁ : List (List α)) (r₂ : List (List α)) :
    List.sublists'Aux a r₁ r₂ = r₂ ++ List.map (List.cons a) r₁
    @[simp]
    theorem List.sublists'_cons {α : Type u} (a : α) (l : List α) :
    (a :: l).sublists' = l.sublists' ++ List.map (List.cons a) l.sublists'
    @[simp]
    theorem List.mem_sublists' {α : Type u} {s : List α} {t : List α} :
    s t.sublists' s.Sublist t
    @[simp]
    theorem List.length_sublists' {α : Type u} (l : List α) :
    l.sublists'.length = 2 ^ l.length
    @[simp]
    theorem List.sublists_nil {α : Type u} :
    [].sublists = [[]]
    @[simp]
    theorem List.sublists_singleton {α : Type u} (a : α) :
    [a].sublists = [[], [a]]
    def List.sublistsAux {α : Type u} (a : α) (r : List (List α)) :
    List (List α)

    Auxiliary helper function for sublists

    Equations
    Instances For
      theorem List.sublistsAux_eq_array_foldl {α : Type u} :
      List.sublistsAux = fun (a : α) (r : List (List α)) => (Array.foldl (fun (r : Array (List α)) (l : List α) => (r.push l).push (a :: l)) #[] r.toArray).toList
      theorem List.sublistsAux_eq_bind {α : Type u} :
      List.sublistsAux = fun (a : α) (r : List (List α)) => r.bind fun (l : List α) => [l, a :: l]
      theorem List.sublists_append {α : Type u} (l₁ : List α) (l₂ : List α) :
      (l₁ ++ l₂).sublists = do let xl₂.sublists List.map (fun (x_1 : List α) => x_1 ++ x) l₁.sublists
      theorem List.sublists_cons {α : Type u} (a : α) (l : List α) :
      (a :: l).sublists = do let xl.sublists [x, a :: x]
      @[simp]
      theorem List.sublists_concat {α : Type u} (l : List α) (a : α) :
      (l ++ [a]).sublists = l.sublists ++ List.map (fun (x : List α) => x ++ [a]) l.sublists
      theorem List.sublists_reverse {α : Type u} (l : List α) :
      l.reverse.sublists = List.map List.reverse l.sublists'
      theorem List.sublists_eq_sublists' {α : Type u} (l : List α) :
      l.sublists = List.map List.reverse l.reverse.sublists'
      theorem List.sublists'_reverse {α : Type u} (l : List α) :
      l.reverse.sublists' = List.map List.reverse l.sublists
      theorem List.sublists'_eq_sublists {α : Type u} (l : List α) :
      l.sublists' = List.map List.reverse l.reverse.sublists
      @[simp]
      theorem List.mem_sublists {α : Type u} {s : List α} {t : List α} :
      s t.sublists s.Sublist t
      @[simp]
      theorem List.length_sublists {α : Type u} (l : List α) :
      l.sublists.length = 2 ^ l.length
      theorem List.map_pure_sublist_sublists {α : Type u} (l : List α) :
      (List.map pure l).Sublist l.sublists
      @[deprecated List.map_pure_sublist_sublists]
      theorem List.map_ret_sublist_sublists {α : Type u} (l : List α) :
      (List.map List.ret l).Sublist l.sublists

      sublistsLen #

      def List.sublistsLenAux {α : Type u} {β : Type v} :
      List α(List αβ)List βList β

      Auxiliary function to construct the list of all sublists of a given length. Given an integer n, a list l, a function f and an auxiliary list L, it returns the list made of f applied to all sublists of l of length n, concatenated with L.

      Equations
      Instances For
        def List.sublistsLen {α : Type u} (n : ) (l : List α) :
        List (List α)

        The list of all sublists of a list l that are of length n. For instance, for l = [0, 1, 2, 3] and n = 2, one gets [[2, 3], [1, 3], [1, 2], [0, 3], [0, 2], [0, 1]].

        Equations
        Instances For
          theorem List.sublistsLenAux_append {α : Type u} {β : Type v} {γ : Type w} (n : ) (l : List α) (f : List αβ) (g : βγ) (r : List β) (s : List γ) :
          theorem List.sublistsLenAux_eq {α : Type u} {β : Type v} (l : List α) (n : ) (f : List αβ) (r : List β) :
          theorem List.sublistsLenAux_zero {α : Type u} {β : Type v} (l : List α) (f : List αβ) (r : List β) :
          List.sublistsLenAux 0 l f r = f [] :: r
          @[simp]
          theorem List.sublistsLen_zero {α : Type u} (l : List α) :
          @[simp]
          theorem List.sublistsLen_succ_nil {α : Type u} (n : ) :
          List.sublistsLen (n + 1) [] = []
          @[simp]
          theorem List.sublistsLen_succ_cons {α : Type u} (n : ) (a : α) (l : List α) :
          theorem List.sublistsLen_one {α : Type u} (l : List α) :
          List.sublistsLen 1 l = List.map (fun (x : α) => [x]) l.reverse
          @[simp]
          theorem List.length_sublistsLen {α : Type u} (n : ) (l : List α) :
          (List.sublistsLen n l).length = l.length.choose n
          theorem List.sublistsLen_sublist_sublists' {α : Type u} (n : ) (l : List α) :
          (List.sublistsLen n l).Sublist l.sublists'
          theorem List.sublistsLen_sublist_of_sublist {α : Type u} (n : ) {l₁ : List α} {l₂ : List α} (h : l₁.Sublist l₂) :
          (List.sublistsLen n l₁).Sublist (List.sublistsLen n l₂)
          theorem List.length_of_sublistsLen {α : Type u} {n : } {l : List α} {l' : List α} :
          l' List.sublistsLen n ll'.length = n
          theorem List.mem_sublistsLen_self {α : Type u} {l : List α} {l' : List α} (h : l'.Sublist l) :
          l' List.sublistsLen l'.length l
          @[simp]
          theorem List.mem_sublistsLen {α : Type u} {n : } {l : List α} {l' : List α} :
          l' List.sublistsLen n l l'.Sublist l l'.length = n
          theorem List.sublistsLen_of_length_lt {α : Type u} {n : } {l : List α} (h : l.length < n) :
          @[simp]
          theorem List.sublistsLen_length {α : Type u} (l : List α) :
          List.sublistsLen l.length l = [l]
          theorem List.Pairwise.sublists' {α : Type u} {R : ααProp} {l : List α} :
          theorem List.pairwise_sublists {α : Type u} {R : ααProp} {l : List α} (H : List.Pairwise R l) :
          List.Pairwise (fun (l₁ l₂ : List α) => List.Lex R l₁.reverse l₂.reverse) l.sublists
          @[simp]
          theorem List.nodup_sublists {α : Type u} {l : List α} :
          l.sublists.Nodup l.Nodup
          @[simp]
          theorem List.nodup_sublists' {α : Type u} {l : List α} :
          l.sublists'.Nodup l.Nodup
          theorem List.nodup.sublists {α : Type u} {l : List α} :
          l.Nodupl.sublists.Nodup

          Alias of the reverse direction of List.nodup_sublists.

          theorem List.nodup.of_sublists {α : Type u} {l : List α} :
          l.sublists.Nodupl.Nodup

          Alias of the forward direction of List.nodup_sublists.

          theorem List.nodup.sublists' {α : Type u} {l : List α} :
          l.Nodupl.sublists'.Nodup

          Alias of the reverse direction of List.nodup_sublists'.

          theorem List.nodup.of_sublists' {α : Type u} {l : List α} :
          l.sublists'.Nodupl.Nodup

          Alias of the forward direction of List.nodup_sublists'.

          theorem List.nodup_sublistsLen {α : Type u} (n : ) {l : List α} (h : l.Nodup) :
          (List.sublistsLen n l).Nodup
          theorem List.sublists_map {α : Type u} {β : Type v} (f : αβ) (l : List α) :
          (List.map f l).sublists = List.map (List.map f) l.sublists
          theorem List.sublists'_map {α : Type u} {β : Type v} (f : αβ) (l : List α) :
          (List.map f l).sublists' = List.map (List.map f) l.sublists'
          theorem List.sublists_perm_sublists' {α : Type u} (l : List α) :
          l.sublists.Perm l.sublists'
          theorem List.sublists_cons_perm_append {α : Type u} (a : α) (l : List α) :
          (a :: l).sublists.Perm (l.sublists ++ List.map (List.cons a) l.sublists)
          theorem List.revzip_sublists {α : Type u} (l : List α) (l₁ : List α) (l₂ : List α) :
          (l₁, l₂) l.sublists.revzip(l₁ ++ l₂).Perm l
          theorem List.revzip_sublists' {α : Type u} (l : List α) (l₁ : List α) (l₂ : List α) :
          (l₁, l₂) l.sublists'.revzip(l₁ ++ l₂).Perm l
          theorem List.range_bind_sublistsLen_perm {α : Type u} (l : List α) :
          ((List.range (l.length + 1)).bind fun (n : ) => List.sublistsLen n l).Perm l.sublists'