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} : List.sublists' [] = [[]]

@[simp]

theorem List.sublists'_singleton {α : Type u} (a : α) : List.sublists' [a] = [[], [a]]

def List.sublists'Aux {α : Type u} (a : α) (r₁ : List (List α)) (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₁

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)) (List.toArray r₂) (List.toArray r₁) 0 (Array.size (List.toArray r₁)))

theorem List.sublists'_eq_sublists'Aux {α : Type u} (l : List α) : List.sublists' l = 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 α) : List.sublists' (a :: l) = List.sublists' l ++ List.map (List.cons a) (List.sublists' l)

@[simp]

theorem List.mem_sublists' {α : Type u} {s : List α} {t : List α} : s ∈ List.sublists' t ↔ List.Sublist s t

@[simp]

theorem List.length_sublists' {α : Type u} (l : List α) : List.length (List.sublists' l) = 2 ^ List.length l

@[simp]

theorem List.sublists_nil {α : Type u} : List.sublists [] = [[]]

@[simp]

theorem List.sublists_singleton {α : Type u} (a : α) : List.sublists [a] = [[], [a]]

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

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 (Array.push r l) (a :: l)) #[] (List.toArray r) 0 (Array.size (List.toArray r)))

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_eq_sublistsFast : @List.sublists = @List.sublistsFast

theorem List.sublists_append {α : Type u} (l₁ : List α) (l₂ : List α) : List.sublists (l₁ ++ l₂) = do let x ← List.sublists l₂ List.map (fun (x_1 : List α) => x_1 ++ x) (List.sublists l₁)

theorem List.sublists_cons {α : Type u} (a : α) (l : List α) : List.sublists (a :: l) = do let x ← List.sublists l [x, a :: x]

@[simp]

theorem List.sublists_concat {α : Type u} (l : List α) (a : α) : List.sublists (l ++ [a]) = List.sublists l ++ List.map (fun (x : List α) => x ++ [a]) (List.sublists l)

theorem List.sublists_reverse {α : Type u} (l : List α) : List.sublists (List.reverse l) = List.map List.reverse (List.sublists' l)

theorem List.sublists_eq_sublists' {α : Type u} (l : List α) : List.sublists l = List.map List.reverse (List.sublists' (List.reverse l))

theorem List.sublists'_reverse {α : Type u} (l : List α) : List.sublists' (List.reverse l) = List.map List.reverse (List.sublists l)

theorem List.sublists'_eq_sublists {α : Type u} (l : List α) : List.sublists' l = List.map List.reverse (List.sublists (List.reverse l))

@[simp]

theorem List.mem_sublists {α : Type u} {s : List α} {t : List α} : s ∈ List.sublists t ↔ List.Sublist s t

@[simp]

theorem List.length_sublists {α : Type u} (l : List α) : List.length (List.sublists l) = 2 ^ List.length l

theorem List.map_ret_sublist_sublists {α : Type u} (l : List α) : List.Sublist (List.map List.ret l) (List.sublists 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

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

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

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

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 (List.sublistsLenAux n l f r) ++ s

theorem List.sublistsLenAux_eq {α : Type u_1} {β : Type u_2} (l : List α) (n : ℕ) (f : List α → β) (r : List β) : List.sublistsLenAux n l f r = List.map f (List.sublistsLen n l) ++ r

theorem List.sublistsLenAux_zero {β : Type v} {α : Type u_1} (l : List α) (f : List α → β) (r : List β) : List.sublistsLenAux 0 l f r = f [] :: r

@[simp]

theorem List.sublistsLen_zero {α : Type u_1} (l : List α) : List.sublistsLen 0 l = [[]]

@[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 (List.cons a) (List.sublistsLen n l)

@[simp]

theorem List.length_sublistsLen {α : Type u_1} (n : ℕ) (l : List α) : List.length (List.sublistsLen n l) = Nat.choose (List.length l) n

theorem List.sublistsLen_sublist_sublists' {α : Type u_1} (n : ℕ) (l : List α) : List.Sublist (List.sublistsLen n l) (List.sublists' l)

theorem List.sublistsLen_sublist_of_sublist {α : Type u_1} (n : ℕ) {l₁ : List α} {l₂ : List α} (h : List.Sublist l₁ l₂) : List.Sublist (List.sublistsLen n l₁) (List.sublistsLen n l₂)

theorem List.length_of_sublistsLen {α : Type u_1} {n : ℕ} {l : List α} {l' : List α} : l' ∈ List.sublistsLen n l → List.length l' = n

theorem List.mem_sublistsLen_self {α : Type u_1} {l : List α} {l' : List α} (h : List.Sublist l' l) : l' ∈ List.sublistsLen (List.length l') l

@[simp]

theorem List.mem_sublistsLen {α : Type u_1} {n : ℕ} {l : List α} {l' : List α} : l' ∈ List.sublistsLen n l ↔ List.Sublist l' l ∧ List.length l' = n

theorem List.sublistsLen_of_length_lt {α : Type u} {n : ℕ} {l : List α} (h : List.length l < n) : List.sublistsLen n l = []

@[simp]

theorem List.sublistsLen_length {α : Type u} (l : List α) : List.sublistsLen (List.length l) l = [l]

theorem List.Pairwise.sublists' {α : Type u} {R : α → α → Prop} {l : List α} : List.Pairwise R l → List.Pairwise (List.Lex (Function.swap R)) (List.sublists' l)

theorem List.pairwise_sublists {α : Type u} {R : α → α → Prop} {l : List α} (H : List.Pairwise R l) : List.Pairwise (fun (l₁ l₂ : List α) => List.Lex R (List.reverse l₁) (List.reverse l₂)) (List.sublists l)

@[simp]

theorem List.nodup_sublists {α : Type u} {l : List α} : List.Nodup (List.sublists l) ↔ List.Nodup l

@[simp]

theorem List.nodup_sublists' {α : Type u} {l : List α} : List.Nodup (List.sublists' l) ↔ List.Nodup l

theorem List.nodup.of_sublists {α : Type u} {l : List α} : List.Nodup (List.sublists l) → List.Nodup l

Alias of the forward direction of List.nodup_sublists.

theorem List.nodup.sublists {α : Type u} {l : List α} : List.Nodup l → List.Nodup (List.sublists l)

Alias of the reverse direction of List.nodup_sublists.

theorem List.nodup.of_sublists' {α : Type u} {l : List α} : List.Nodup (List.sublists' l) → List.Nodup l

Alias of the forward direction of List.nodup_sublists'.

theorem List.nodup.sublists' {α : Type u} {l : List α} : List.Nodup l → List.Nodup (List.sublists' l)

Alias of the reverse direction of List.nodup_sublists'.

theorem List.nodup_sublistsLen {α : Type u} (n : ℕ) {l : List α} (h : List.Nodup l) : List.Nodup (List.sublistsLen n l)

theorem List.sublists_map {α : Type u} {β : Type v} (f : α → β) (l : List α) : List.sublists (List.map f l) = List.map (List.map f) (List.sublists l)

theorem List.sublists'_map {α : Type u} {β : Type v} (f : α → β) (l : List α) : List.sublists' (List.map f l) = List.map (List.map f) (List.sublists' l)

theorem List.sublists_perm_sublists' {α : Type u} (l : List α) : List.sublists l ~ List.sublists' l

theorem List.sublists_cons_perm_append {α : Type u} (a : α) (l : List α) : List.sublists (a :: l) ~ List.sublists l ++ List.map (List.cons a) (List.sublists l)

theorem List.revzip_sublists {α : Type u} (l : List α) (l₁ : List α) (l₂ : List α) : (l₁, l₂) ∈ List.revzip (List.sublists l) → l₁ ++ l₂ ~ l

theorem List.revzip_sublists' {α : Type u} (l : List α) (l₁ : List α) (l₂ : List α) : (l₁, l₂) ∈ List.revzip (List.sublists' l) → l₁ ++ l₂ ~ l

theorem List.range_bind_sublistsLen_perm {α : Type u_1} (l : List α) : (List.bind (List.range (List.length l + 1)) fun (n : ℕ) => List.sublistsLen n l) ~ List.sublists' l