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.map_sublists'_aux
{α : Type u}
{β : Type v}
{γ : Type w}
(g : list β → list γ)
(l : list α)
(f : list α → list β)
(r : list (list β)) :
list.map g (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 β)) :
l.sublists'_aux f (r ++ r') = l.sublists'_aux f r ++ r'
@[simp]
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_cons_eq_sublists_aux₁
{α : Type u}
(l : list α) :
l.sublists_aux list.cons = 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 = 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 β) :
(a :: l).sublists_aux f = list.foldr f list.nil ((a :: l).sublists_aux list.cons)
theorem
list.sublists_aux_eq_foldr
{α : Type u}
{β : Type v}
(l : list α)
(f : list α → list β → list β) :
l.sublists_aux f = list.foldr f list.nil (l.sublists_aux list.cons)
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)
sublists_len #
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
- list.sublists_len_aux (n + 1) (a :: l) f r = list.sublists_len_aux (n + 1) l f (list.sublists_len_aux n l (f ∘ list.cons a) r)
- list.sublists_len_aux (n + 1) list.nil f r = r
- list.sublists_len_aux 0 (hd :: tl) f r = f list.nil :: r
- list.sublists_len_aux 0 list.nil f r = f list.nil :: r
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 γ) :
list.sublists_len_aux n l (g ∘ f) (list.map g r ++ s) = list.map g (list.sublists_len_aux n l f r) ++ s
theorem
list.sublists_len_aux_eq
{α : Type u_1}
{β : Type u_2}
(l : list α)
(n : ℕ)
(f : list α → β)
(r : list β) :
list.sublists_len_aux n l f r = list.map f (list.sublists_len n l) ++ r
theorem
list.sublists_len_aux_zero
{β : Type v}
{α : Type u_1}
(l : list α)
(f : list α → β)
(r : list β) :
list.sublists_len_aux 0 l f r = f list.nil :: r
@[simp]
@[simp]
theorem
list.sublists_len_succ_nil
{α : Type u_1}
(n : ℕ) :
list.sublists_len (n + 1) list.nil = list.nil
@[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 ++ list.map (list.cons a) (list.sublists_len n l)
@[simp]
theorem
list.length_sublists_len
{α : Type u_1}
(n : ℕ)
(l : list α) :
(list.sublists_len n l).length = l.length.choose n
theorem
list.sublists_len_sublist_sublists'
{α : Type u_1}
(n : ℕ)
(l : list α) :
list.sublists_len n l <+ l.sublists'
theorem
list.sublists_len_sublist_of_sublist
{α : Type u_1}
(n : ℕ)
{l₁ l₂ : list α}
(h : l₁ <+ l₂) :
list.sublists_len n l₁ <+ list.sublists_len n l₂
theorem
list.length_of_sublists_len
{α : Type u_1}
{n : ℕ}
{l l' : list α} :
l' ∈ list.sublists_len n l → l'.length = n
theorem
list.mem_sublists_len_self
{α : Type u_1}
{l l' : list α}
(h : l' <+ l) :
l' ∈ list.sublists_len l'.length l