# mathlibdocumentation

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].sublists' = [list.nil, [a]]
theorem list.map_sublists'_aux {α : Type u} {β : Type v} {γ : Type w} (g : list βlist γ) (l : list α) (f : list αlist β) (r : list (list β)) :
(l.sublists'_aux f r) = l.sublists'_aux (g f) (list.map g r)
theorem list.sublists'_aux_append {α : Type u} {β : Type v} (r' : list (list β)) (l : list α) (f : list αlist β) (r : list (list β)) :
(r ++ r') = r ++ r'
theorem list.sublists'_aux_eq_sublists' {α : Type u} {β : Type v} (l : list α) (f : list αlist β) (r : list (list β)) :
r = ++ 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]
theorem list.sublists_nil {α : Type u} :
@[simp]
theorem list.sublists_singleton {α : Type u} (a : α) :
[a].sublists = [list.nil, [a]]
theorem list.sublists_aux₁_eq_sublists_aux {α : Type u} {β : Type v} (l : list α) (f : list αlist β) :
= l.sublists_aux (λ (ys : list α) (r : list β), f ys ++ r)
theorem list.sublists_aux_cons_eq_sublists_aux₁ {α : Type u} (l : list α) :
= l.sublists_aux₁ (λ (x : list α), [x])
theorem list.sublists_aux_eq_foldr.aux {α : Type u} {β : Type v} {a : α} {l : list α} (IH₁ : ∀ (f : list αlist βlist β), l.sublists_aux f = ) (IH₂ : ∀ (f : list αlist (list α)list (list α)), l.sublists_aux f = ) (f : list αlist βlist β) :
theorem list.sublists_aux_eq_foldr {α : Type u} {β : Type v} (l : list α) (f : list αlist βlist β) :
theorem list.sublists_aux_cons_cons {α : Type u} (l : list α) (a : α) :
(a :: l).sublists_aux list.cons = [a] :: list.foldr (λ (ys : list α) (r : list (list α)), ys :: (a :: ys) :: r) list.nil
theorem list.sublists_aux₁_append {α : Type u} {β : Type v} (l₁ l₂ : list α) (f : list αlist β) :
(l₁ ++ l₂).sublists_aux₁ f = l₁.sublists_aux₁ f ++ l₂.sublists_aux₁ (λ (x : list α), f x ++ l₁.sublists_aux₁ (f λ (_x : list α), _x ++ x))
theorem list.sublists_aux₁_concat {α : Type u} {β : Type v} (l : list α) (a : α) (f : list αlist β) :
(l ++ [a]).sublists_aux₁ f = ++ f [a] ++ l.sublists_aux₁ (λ (x : list α), f (x ++ [a]))
theorem list.sublists_aux₁_bind {α : Type u} {β : Type v} {γ : Type w} (l : list α) (f : list αlist β) (g : β → list γ) :
(l.sublists_aux₁ f).bind g = l.sublists_aux₁ (λ (x : list α), (f x).bind g)
theorem list.sublists_aux_cons_append {α : Type u} (l₁ l₂ : list α) :
(l₁ ++ l₂).sublists_aux list.cons = ++ >>= λ (x : list α), (λ (_x : list α), _x ++ x) <$> l₁.sublists) theorem list.sublists_append {α : Type u} (l₁ l₂ : list α) : (l₁ ++ l₂).sublists = l₂.sublists >>= λ (x : list α), (λ (_x : list α), _x ++ x) <$> l₁.sublists
@[simp]
theorem list.sublists_concat {α : Type u} (l : list α) (a : α) :
(l ++ [a]).sublists = l.sublists ++ list.map (λ (x : list α), x ++ [a]) l.sublists
theorem list.sublists_reverse {α : Type u} (l : list α) :
theorem list.sublists_eq_sublists' {α : Type u} (l : list α) :
theorem list.sublists'_reverse {α : Type u} (l : list α) :
theorem list.sublists'_eq_sublists {α : Type u} (l : list α) :
theorem list.sublists_aux_ne_nil {α : Type u} (l : list α) :
@[simp]
theorem list.mem_sublists {α : Type u} {s t : list α} :
s t.sublists s <+ t
@[simp]
theorem list.length_sublists {α : Type u} (l : list α) :
theorem list.map_ret_sublist_sublists {α : Type u} (l : list α) :

### sublists_len #

def list.sublists_len_aux {α : 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 of f applied to all sublists of l of length n, concatenated with L.

Equations
def list.sublists_len {α : 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
theorem list.sublists_len_aux_append {α : Type u_1} {β : Type u_2} {γ : Type u_3} (n : ) (l : list α) (f : list α → β) (g : β → γ) (r : list β) (s : list γ) :
(g f) (list.map g r ++ s) = f r) ++ s
theorem list.sublists_len_aux_eq {α : Type u_1} {β : Type u_2} (l : list α) (n : ) (f : list α → β) (r : list β) :
r = l) ++ r
theorem list.sublists_len_aux_zero {β : Type v} {α : Type u_1} (l : list α) (f : list α → β) (r : list β) :
r = :: r
@[simp]
theorem list.sublists_len_zero {α : Type u_1} (l : list α) :
@[simp]
theorem list.sublists_len_succ_nil {α : Type u_1} (n : ) :
@[simp]
theorem list.sublists_len_succ_cons {α : Type u_1} (n : ) (a : α) (l : list α) :
list.sublists_len (n + 1) (a :: l) = list.sublists_len (n + 1) l ++ l)
@[simp]
theorem list.length_sublists_len {α : Type u_1} (n : ) (l : list α) :
theorem list.sublists_len_sublist_sublists' {α : Type u_1} (n : ) (l : list α) :
theorem list.sublists_len_sublist_of_sublist {α : Type u_1} (n : ) {l₁ l₂ : list α} (h : l₁ <+ l₂) :
<+
theorem list.length_of_sublists_len {α : Type u_1} {n : } {l l' : list α} :
l' l'.length = n
theorem list.mem_sublists_len_self {α : Type u_1} {l l' : list α} (h : l' <+ l) :
l'
@[simp]
theorem list.mem_sublists_len {α : Type u_1} {n : } {l l' : list α} :
l' l' <+ l l'.length = n
theorem list.sublists_len_of_length_lt {α : Type u} {n : } {l : list α} (h : l.length < n) :
@[simp]
theorem list.sublists_len_length {α : Type u} (l : list α) :
= [l]