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]
@[simp]
theorem List.sublists'_singleton {α : Type u} (a : α) :
def List.sublists'Aux {α : Type u} (a : α) (r₁ r₂ : List (List α)) :
List (List α)

Auxiliary helper definition for sublists'

Equations
    Instances For
      theorem List.sublists'Aux_eq_array_foldl {α : Type u} (a : α) (r₁ r₂ : 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' = foldr (fun (a : α) (r : List (List α)) => sublists'Aux a r r) [[]] l
      theorem List.sublists'Aux_eq_map {α : Type u} (a : α) (r₁ r₂ : List (List α)) :
      sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁
      @[simp]
      theorem List.sublists'_cons {α : Type u} (a : α) (l : List α) :
      @[simp]
      theorem List.mem_sublists' {α : Type u} {s t : List α} :
      @[simp]
      theorem List.length_sublists' {α : Type u} (l : List α) :
      @[simp]
      @[simp]
      theorem List.sublists_singleton {α : Type u} (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} :
          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_flatMap {α : Type u} :
          sublistsAux = fun (a : α) (r : List (List α)) => flatMap (fun (l : List α) => [l, a :: l]) r
          theorem List.sublists_append {α : Type u} (l₁ l₂ : List α) :
          (l₁ ++ l₂).sublists = do let xl₂.sublists 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 ++ map (fun (x : List α) => x ++ [a]) l.sublists
          @[simp]
          theorem List.mem_sublists {α : Type u} {s t : List α} :
          @[simp]
          theorem List.length_sublists {α : Type u} (l : List α) :

          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 γ) :
                  sublistsLenAux n l (g f) (map g r ++ s) = map g (sublistsLenAux n l f r) ++ s
                  theorem List.sublistsLenAux_eq {α : Type u} {β : Type v} (l : List α) (n : ) (f : List αβ) (r : List β) :
                  sublistsLenAux n l f r = map f (sublistsLen n l) ++ r
                  theorem List.sublistsLenAux_zero {α : Type u} {β : Type v} (l : List α) (f : List αβ) (r : 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 : ) :
                  @[simp]
                  theorem List.sublistsLen_succ_cons {α : Type u} (n : ) (a : α) (l : List α) :
                  sublistsLen (n + 1) (a :: l) = sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)
                  theorem List.sublistsLen_one {α : Type u} (l : List α) :
                  sublistsLen 1 l = map (fun (x : α) => [x]) l.reverse
                  @[simp]
                  theorem List.length_sublistsLen {α : Type u} (n : ) (l : List α) :
                  theorem List.sublistsLen_sublist_of_sublist {α : Type u} (n : ) {l₁ l₂ : List α} (h : l₁.Sublist l₂) :
                  (sublistsLen n l₁).Sublist (sublistsLen n l₂)
                  theorem List.length_of_sublistsLen {α : Type u} {n : } {l l' : List α} :
                  l' sublistsLen n ll'.length = n
                  theorem List.mem_sublistsLen_self {α : Type u} {l l' : List α} (h : l'.Sublist l) :
                  @[simp]
                  theorem List.mem_sublistsLen {α : Type u} {n : } {l l' : List α} :
                  l' 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 α) :
                  theorem List.Pairwise.sublists' {α : Type u} {R : ααProp} {l : List α} :
                  theorem List.pairwise_sublists {α : Type u} {R : ααProp} {l : List α} (H : Pairwise R l) :
                  @[simp]
                  theorem List.nodup_sublists {α : Type u} {l : List α} :
                  @[simp]
                  theorem List.nodup_sublists' {α : Type u} {l : List α} :
                  theorem List.Nodup.of_sublists {α : Type u} {l : List α} :

                  Alias of the forward direction of List.nodup_sublists.

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

                  Alias of the reverse direction of List.nodup_sublists.

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

                  Alias of the forward direction of List.nodup_sublists'.

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