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]

theorem list.sublists'_nil {α : Type u} :

list.nil.sublists' = [list.nil]

@[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 β)) :

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'

theorem list.sublists'_aux_eq_sublists' {α : Type u} {β : Type v} (l : list α) (f : list α → list β) (r : list (list β)) :

l.sublists'_aux f r = list.map f l.sublists' ++ r

@[simp]

theorem list.sublists'_cons {α : Type u} (a : α) (l : list α) :

(a :: l).sublists' = l.sublists' ++ list.map (list.cons 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 α) :

l.sublists'.length = 2 ^ l.length

@[simp]

theorem list.sublists_nil {α : Type u} :

list.nil.sublists = [list.nil]

@[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₁ 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)

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 α) :

l.reverse.sublists = list.map list.reverse l.sublists'

theorem list.sublists_eq_sublists' {α : Type u} (l : list α) :

l.sublists = list.map list.reverse l.reverse.sublists'

theorem list.sublists'_reverse {α : Type u} (l : list α) :

l.reverse.sublists' = list.map list.reverse l.sublists

theorem list.sublists'_eq_sublists {α : Type u} (l : list α) :

l.sublists' = list.map list.reverse l.reverse.sublists

theorem list.sublists_aux_ne_nil {α : Type u} (l : list α) :

list.nil ∉ l.sublists_aux list.cons

@[simp]

theorem list.mem_sublists {α : Type u} {s t : list α} :

s ∈ t.sublists ↔ s <+ t

@[simp]

theorem list.length_sublists {α : Type u} (l : list α) :

l.sublists.length = 2 ^ l.length

theorem list.map_ret_sublist_sublists {α : Type u} (l : list α) :

list.map list.ret l <+ l.sublists

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

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

def list.sublists_len {α : Type u_1} (n : ℕ) (l : 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.sublists_len n l = list.sublists_len_aux n l id list.nil

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]

theorem list.sublists_len_zero {α : Type u_1} (l : list α) :

list.sublists_len 0 l = [list.nil]

@[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

@[simp]

theorem list.mem_sublists_len {α : Type u_1} {n : ℕ} {l l' : list α} :

l' ∈ list.sublists_len n l ↔ l' <+ l ∧ l'.length = n

theorem list.sublists_len_of_length_lt {α : Type u} {n : ℕ} {l : list α} (h : l.length < n) :

list.sublists_len n l = list.nil

@[simp]

theorem list.sublists_len_length {α : Type u} (l : list α) :

list.sublists_len l.length l = [l]

theorem list.pairwise.sublists' {α : Type u} {R : α → α → Prop} {l : list α} :

list.pairwise R l → list.pairwise (list.lex (function.swap R)) l.sublists'

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 α} :

l.sublists.nodup ↔ l.nodup

@[simp]

theorem list.nodup_sublists' {α : Type u} {l : list α} :

l.sublists'.nodup ↔ l.nodup

theorem list.nodup.of_sublists {α : Type u} {l : list α} :

l.sublists.nodup → l.nodup

Alias of the forward direction of list.nodup_sublists.

@[protected]

theorem list.nodup.sublists {α : Type u} {l : list α} :

l.nodup → l.sublists.nodup

Alias of the reverse direction of list.nodup_sublists.

theorem list.nodup.of_sublists' {α : Type u} {l : list α} :

l.sublists'.nodup → l.nodup

Alias of the forward direction of list.nodup_sublists'.

@[protected]

theorem list.nodup.sublists' {α : Type u} {l : list α} :

l.nodup → l.sublists'.nodup

Alias of the reverse direction of list.nodup_sublists'.

theorem list.nodup_sublists_len {α : Type u} (n : ℕ) {l : list α} (h : l.nodup) :

(list.sublists_len n l).nodup

theorem list.sublists_cons_perm_append {α : Type u} (a : α) (l : list α) :

(a :: l).sublists ~ l.sublists ++ list.map (list.cons a) l.sublists

theorem list.sublists_perm_sublists' {α : Type u} (l : list α) :

l.sublists ~ l.sublists'

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 α) :

(list.range (l.length + 1)).bind (λ (n : ℕ), list.sublists_len n l) ~ l.sublists'