# 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} :
= [[]]
@[simp]
theorem List.sublists'_singleton {α : Type u} (a : α) :
= [[], [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.toList (Array.foldl (fun (r : Array (List α)) (l : List α) => Array.push r (a :: l)) () () 0 ())
theorem List.sublists'_eq_sublists'Aux {α : Type u} (l : List α) :
= List.foldr (fun (a : α) (r : List (List α)) => ) [[]] 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 () r₁
@[simp]
theorem List.sublists'_cons {α : Type u} (a : α) (l : List α) :
@[simp]
theorem List.mem_sublists' {α : Type u} {s : List α} {t : List α} :
@[simp]
theorem List.length_sublists' {α : Type u} (l : List α) :
= 2 ^
@[simp]
theorem List.sublists_nil {α : Type u} :
= [[]]
@[simp]
theorem List.sublists_singleton {α : Type u} (a : α) :
= [[], [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.toList (Array.foldl (fun (r : Array (List α)) (l : List α) => Array.push () (a :: l)) #[] () 0 ())
theorem List.sublistsAux_eq_bind {α : Type u} :
List.sublistsAux = fun (a : α) (r : List (List α)) => List.bind r fun (l : List α) => [l, a :: l]
@[csimp]
theorem List.sublists_append {α : Type u} (l₁ : List α) (l₂ : List α) :
List.sublists (l₁ ++ l₂) = do let x ← List.map (fun (x_1 : List α) => x_1 ++ x) ()
theorem List.sublists_cons {α : Type u} (a : α) (l : List α) :
List.sublists (a :: l) = do let x ← [x, a :: x]
@[simp]
theorem List.sublists_concat {α : Type u} (l : List α) (a : α) :
List.sublists (l ++ [a]) = ++ List.map (fun (x : List α) => x ++ [a]) ()
theorem List.sublists_reverse {α : Type u} (l : List α) :
= List.map List.reverse ()
theorem List.sublists_eq_sublists' {α : Type u} (l : List α) :
= List.map List.reverse ()
theorem List.sublists'_reverse {α : Type u} (l : List α) :
= List.map List.reverse ()
theorem List.sublists'_eq_sublists {α : Type u} (l : List α) :
= List.map List.reverse ()
@[simp]
theorem List.mem_sublists {α : Type u} {s : List α} {t : List α} :
@[simp]
theorem List.length_sublists {α : Type u} (l : List α) :
= 2 ^
theorem List.map_ret_sublist_sublists {α : Type u} (l : List α) :
List.Sublist (List.map List.ret l) ()

### sublistsLen #

def List.sublistsLenAux {α : Type u_1} {β : Type u_2} :
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_1} (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_1} {β : Type u_2} {γ : Type u_3} (n : ) (l : List α) (f : List αβ) (g : βγ) (r : List β) (s : List γ) :
List.sublistsLenAux n l (g f) (List.map g r ++ s) = List.map g () ++ s
theorem List.sublistsLenAux_eq {α : Type u_1} {β : Type u_2} (l : List α) (n : ) (f : List αβ) (r : List β) :
= List.map f () ++ r
theorem List.sublistsLenAux_zero {β : Type v} {α : Type u_1} (l : List α) (f : List αβ) (r : List β) :
= f [] :: r
@[simp]
theorem List.sublistsLen_zero {α : Type u_1} (l : List α) :
= [[]]
@[simp]
theorem List.sublistsLen_succ_nil {α : Type u_1} (n : ) :
List.sublistsLen (n + 1) [] = []
@[simp]
theorem List.sublistsLen_succ_cons {α : Type u_1} (n : ) (a : α) (l : List α) :
List.sublistsLen (n + 1) (a :: l) = List.sublistsLen (n + 1) l ++ List.map () ()
@[simp]
theorem List.length_sublistsLen {α : Type u_1} (n : ) (l : List α) :
=
theorem List.sublistsLen_sublist_sublists' {α : Type u_1} (n : ) (l : List α) :
theorem List.sublistsLen_sublist_of_sublist {α : Type u_1} (n : ) {l₁ : List α} {l₂ : List α} (h : List.Sublist l₁ l₂) :
theorem List.length_of_sublistsLen {α : Type u_1} {n : } {l : List α} {l' : List α} :
l' = n
theorem List.mem_sublistsLen_self {α : Type u_1} {l : List α} {l' : List α} (h : List.Sublist l' l) :
l'
@[simp]
theorem List.mem_sublistsLen {α : Type u_1} {n : } {l : List α} {l' : List α} :
theorem List.sublistsLen_of_length_lt {α : Type u} {n : } {l : List α} (h : < n) :
= []
@[simp]
theorem List.sublistsLen_length {α : Type u} (l : List α) :
= [l]
theorem List.Pairwise.sublists' {α : Type u} {R : ααProp} {l : List α} :
theorem List.pairwise_sublists {α : Type u} {R : ααProp} {l : List α} (H : ) :
List.Pairwise (fun (l₁ l₂ : List α) => List.Lex R () ()) ()
@[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.sublists' {α : Type u} {l : List α} :

Alias of the reverse direction of List.nodup_sublists'.

theorem List.nodup_sublistsLen {α : Type u} (n : ) {l : List α} (h : ) :
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_perm_sublists' {α : Type u} (l : List α) :
theorem List.sublists_cons_perm_append {α : Type u} (a : α) (l : List α) :
theorem List.revzip_sublists {α : Type u} (l : List α) (l₁ : List α) (l₂ : List α) :
(l₁, l₂) l₁ ++ l₂ ~ l
theorem List.revzip_sublists' {α : Type u} (l : List α) (l₁ : List α) (l₂ : List α) :
(l₁, l₂) l₁ ++ l₂ ~ l
theorem List.range_bind_sublistsLen_perm {α : Type u_1} (l : List α) :
(List.bind (List.range ( + 1)) fun (n : ) => ) ~