# sublists #

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

This file contains basic results on this function.

### sublists #

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

Auxiliary helper definition for `sublists'`

Equations

- List.sublists'Aux a r₁ r₂ = List.foldl (fun (r : List (List α)) (l : List α) => r ++ [a :: l]) r₂ r₁

Instances For

source
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
source
theorem List.sublists'_eq_sublists'Aux {α : Type u} (l : List α) :
l.sublists' = foldr (fun (a : α) (r : List (List α)) => sublists'Aux a r r) [[]] l
source
theorem List.sublists'Aux_eq_map {α : Type u} (a : α) (r₁ r₂ : List (List α)) :
sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁
source
@[simp]
theorem List.sublists'_cons {α : Type u} (a : α) (l : List α) :
(a :: l).sublists' = l.sublists' ++ map (cons a) l.sublists'
source
@[simp]
theorem List.mem_sublists' {α : Type u} {s t : List α} :
s ∈ t.sublists' ↔ s.Sublist t
source
@[simp]
theorem List.length_sublists' {α : Type u} (l : List α) :
l.sublists'.length = 2 ^ l.length
source
@[simp]
theorem List.sublists_nil {α : Type u} :
[].sublists = [[]]
source
@[simp]
theorem List.sublists_singleton {α : Type u} (a : α) :
[a].sublists = [[], [a]]
source
def List.sublistsAux {α : Type u} (a : α) (r : List (List α)) :
List (List α)

Auxiliary helper function for `sublists`

Equations

- List.sublistsAux a r = List.foldl (fun (r : List (List α)) (l : List α) => r ++ [l, a :: l]) [] r

Instances For

source
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
source
theorem List.sublistsAux_eq_flatMap {α : Type u} :
sublistsAux = fun (a : α) (r : List (List α)) => flatMap (fun (l : List α) => [l, a :: l]) r
source
theorem List.sublists_append {α : Type u} (l₁ l₂ : List α) :
(l₁ ++ l₂).sublists = do let x ← l₂.sublists map (fun (x_1 : List α) => x_1 ++ x) l₁.sublists
source
theorem List.sublists_cons {α : Type u} (a : α) (l : List α) :
(a :: l).sublists = do let x ← l.sublists [x, a :: x]
source
@[simp]
theorem List.sublists_concat {α : Type u} (l : List α) (a : α) :
(l ++ [a]).sublists = l.sublists ++ map (fun (x : List α) => x ++ [a]) l.sublists
source
theorem List.sublists_reverse {α : Type u} (l : List α) :
l.reverse.sublists = map reverse l.sublists'
source
theorem List.sublists_eq_sublists' {α : Type u} (l : List α) :
l.sublists = map reverse l.reverse.sublists'
source
theorem List.sublists'_reverse {α : Type u} (l : List α) :
l.reverse.sublists' = map reverse l.sublists
source
theorem List.sublists'_eq_sublists {α : Type u} (l : List α) :
l.sublists' = map reverse l.reverse.sublists
source
@[simp]
theorem List.mem_sublists {α : Type u} {s t : List α} :
s ∈ t.sublists ↔ s.Sublist t
source
@[simp]
theorem List.length_sublists {α : Type u} (l : List α) :
l.sublists.length = 2 ^ l.length
source
theorem List.map_pure_sublist_sublists {α : Type u} (l : List α) :
(map pure l).Sublist l.sublists

### sublistsLen #

source
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

- List.sublistsLenAux 0 x✝² x✝¹ x✝ = x✝¹ [] :: x✝
- List.sublistsLenAux n.succ [] x✝¹ x✝ = x✝
- List.sublistsLenAux n.succ (a :: l) x✝¹ x✝ = List.sublistsLenAux (n + 1) l x✝¹ (List.sublistsLenAux n l (x✝¹ ∘ List.cons a) x✝)

Instances For

source
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

- List.sublistsLen n l = List.sublistsLenAux n l id []

Instances For

source
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
source
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
source
theorem List.sublistsLenAux_zero {α : Type u} {β : Type v} (l : List α) (f : List α → β) (r : List β) :
sublistsLenAux 0 l f r = f [] :: r
source
@[simp]
theorem List.sublistsLen_zero {α : Type u} (l : List α) :
sublistsLen 0 l = [[]]
source
@[simp]
theorem List.sublistsLen_succ_nil {α : Type u} (n : ℕ) :
sublistsLen (n + 1) [] = []
source
@[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)
source
theorem List.sublistsLen_one {α : Type u} (l : List α) :
sublistsLen 1 l = map (fun (x : α) => [x]) l.reverse
source
@[simp]
theorem List.length_sublistsLen {α : Type u} (n : ℕ) (l : List α) :
(sublistsLen n l).length = l.length.choose n
source
theorem List.sublistsLen_sublist_sublists' {α : Type u} (n : ℕ) (l : List α) :
(sublistsLen n l).Sublist l.sublists'
source
theorem List.sublistsLen_sublist_of_sublist {α : Type u} (n : ℕ) {l₁ l₂ : List α} (h : l₁.Sublist l₂) :
(sublistsLen n l₁).Sublist (sublistsLen n l₂)
source
theorem List.length_of_sublistsLen {α : Type u} {n : ℕ} {l l' : List α} :
l' ∈ sublistsLen n l → l'.length = n
source
theorem List.mem_sublistsLen_self {α : Type u} {l l' : List α} (h : l'.Sublist l) :
l' ∈ sublistsLen l'.length l
source
@[simp]
theorem List.mem_sublistsLen {α : Type u} {n : ℕ} {l l' : List α} :
l' ∈ sublistsLen n l ↔ l'.Sublist l ∧ l'.length = n
source
theorem List.sublistsLen_of_length_lt {α : Type u} {n : ℕ} {l : List α} (h : l.length < n) :
sublistsLen n l = []
source
@[simp]
theorem List.sublistsLen_length {α : Type u} (l : List α) :
sublistsLen l.length l = [l]
source
theorem List.Pairwise.sublists' {α : Type u} {R : α → α → Prop} {l : List α} :
Pairwise R l → Pairwise (Lex (Function.swap R)) l.sublists'
source
theorem List.pairwise_sublists {α : Type u} {R : α → α → Prop} {l : List α} (H : Pairwise R l) :
Pairwise (Function.onFun (Lex R) reverse) l.sublists
source
@[simp]
theorem List.nodup_sublists {α : Type u} {l : List α} :
l.sublists.Nodup ↔ l.Nodup
source
@[simp]
theorem List.nodup_sublists' {α : Type u} {l : List α} :
l.sublists'.Nodup ↔ l.Nodup
source
theorem List.Nodup.of_sublists {α : Type u} {l : List α} :
l.sublists.Nodup → l.Nodup

Alias of the forward direction of `List.nodup_sublists`.

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

Alias of the reverse direction of `List.nodup_sublists`.

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

Alias of the forward direction of `List.nodup_sublists'`.

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