mathlib3 documentation

data.list.sublists

sublists #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 : α) :
theorem list.map_sublists'_aux {α : Type u} {β : Type v} {γ : Type w} (g : list β list γ) (l : list α) (f : list α list β) (r : list (list β)) :
theorem list.sublists'_aux_append {α : Type u} {β : Type v} (r' : list (list β)) (l : list α) (f : list α list β) (r : list (list β)) :
l.sublists'_aux f (r ++ r') = l.sublists'_aux f r ++ r'
theorem list.sublists'_aux_eq_sublists' {α : Type u} {β : Type v} (l : list α) (f : list α list β) (r : list (list β)) :
@[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 : α) :
theorem list.sublists_aux₁_eq_sublists_aux {α : Type u} {β : Type v} (l : list α) (f : list α list β) :
l.sublists_aux₁ f = l.sublists_aux (λ (ys : list α) (r : list β), f ys ++ r)
theorem list.sublists_aux_eq_foldr.aux {α : Type u} {β : Type v} {a : α} {l : list α} (IH₁ : (f : list α list β list β), l.sublists_aux f = list.foldr f list.nil (l.sublists_aux list.cons)) (IH₂ : (f : list α list (list α) list (list α)), l.sublists_aux f = list.foldr f list.nil (l.sublists_aux list.cons)) (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 (l.sublists_aux list.cons)
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 = l.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 = l₁.sublists_aux list.cons ++ (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
@[simp]
theorem list.mem_sublists {α : Type u} {s t : list α} :
s t.sublists s <+ t
@[simp]
theorem list.length_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 γ) :
theorem list.sublists_len_aux_eq {α : Type u_1} {β : Type u_2} (l : list α) (n : ) (f : list α β) (r : list β) :
theorem list.sublists_len_aux_zero {β : Type v} {α : Type u_1} (l : list α) (f : list α β) (r : list β) :
@[simp]
theorem list.sublists_len_zero {α : Type u_1} (l : list α) :
@[simp]
@[simp]
theorem list.sublists_len_succ_cons {α : Type u_1} (n : ) (a : α) (l : list α) :
@[simp]
theorem list.length_sublists_len {α : 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 α} :
theorem list.mem_sublists_len_self {α : Type u_1} {l l' : list α} (h : l' <+ l) :
@[simp]
theorem list.mem_sublists_len {α : Type u_1} {n : } {l l' : list α} :
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 α) :
theorem list.pairwise.sublists' {α : Type u} {R : α α Prop} {l : list α} :
theorem list.pairwise_sublists {α : Type u} {R : α α Prop} {l : list α} (H : list.pairwise R l) :
list.pairwise (λ (l₁ l₂ : list α), list.lex R l₁.reverse l₂.reverse) l.sublists
@[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.

@[protected]
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'.

@[protected]
theorem list.nodup.sublists' {α : Type u} {l : list α} :

Alias of the reverse direction of list.nodup_sublists'.

theorem list.nodup_sublists_len {α : Type u} (n : ) {l : list α} (h : l.nodup) :
theorem list.sublists_cons_perm_append {α : Type u} (a : α) (l : list α) :
theorem list.sublists_perm_sublists' {α : Type u} (l : list α) :
theorem list.revzip_sublists {α : Type u} (l l₁ l₂ : list α) :
(l₁, l₂) l.sublists.revzip l₁ ++ l₂ ~ l
theorem list.revzip_sublists' {α : Type u} (l l₁ l₂ : list α) :
(l₁, l₂) l.sublists'.revzip l₁ ++ l₂ ~ l
theorem list.range_bind_sublists_len_perm {α : Type u_1} (l : list α) :