mathlib3 documentation

data.list.join

Join of a list of lists #

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

This file proves basic properties of list.join, which concatenates a list of lists. It is defined in data.list.defs.

source
@[simp]
theorem list.join_singleton {α : Type u_1} (l : list α) :
[l].join = l
source
@[simp]
theorem list.join_eq_nil {α : Type u_1} {L : list (list α)} :
L.join = list.nil ↔ ∀ (l : list α), l ∈ L → l = list.nil
source
@[simp]
theorem list.join_append {α : Type u_1} (L₁ L₂ : list (list α)) :
(L₁ ++ L₂).join = L₁.join ++ L₂.join
source
theorem list.join_concat {α : Type u_1} (L : list (list α)) (l : list α) :
(L.concat l).join = L.join ++ l
source
@[simp]
theorem list.join_filter_empty_eq_ff {α : Type u_1} [decidable_pred (λ (l : list α), l.empty = bool.ff)] {L : list (list α)} :
(list.filter (λ (l : list α), l.empty = bool.ff) L).join = L.join
source
@[simp]
theorem list.join_filter_ne_nil {α : Type u_1} [decidable_pred (λ (l : list α), l ≠ list.nil)] {L : list (list α)} :
(list.filter (λ (l : list α), l ≠ list.nil) L).join = L.join
source
theorem list.join_join {α : Type u_1} (l : list (list (list α))) :
l.join.join = (list.map list.join l).join
source
@[simp]
theorem list.length_join {α : Type u_1} (L : list (list α)) :
L.join.length = (list.map list.length L).sum
source
@[simp]
theorem list.length_bind {α : Type u_1} {β : Type u_2} (l : list α) (f : α → list β) :
(l.bind f).length = (list.map (list.length ∘ f) l).sum
source
@[simp]
theorem list.bind_eq_nil {α : Type u_1} {β : Type u_2} {l : list α} {f : α → list β} :
l.bind f = list.nil ↔ ∀ (x : α), x ∈ l → f x = list.nil
source
theorem list.take_sum_join {α : Type u_1} (L : list (list α)) (i : ℕ) :
list.take (list.take i (list.map list.length L)).sum L.join = (list.take i L).join

In a join, taking the first elements up to an index which is the sum of the lengths of the first i sublists, is the same as taking the join of the first i sublists.

source
theorem list.drop_sum_join {α : Type u_1} (L : list (list α)) (i : ℕ) :
list.drop (list.take i (list.map list.length L)).sum L.join = (list.drop i L).join

In a join, dropping all the elements up to an index which is the sum of the lengths of the first i sublists, is the same as taking the join after dropping the first i sublists.

source
theorem list.drop_take_succ_eq_cons_nth_le {α : Type u_1} (L : list α) {i : ℕ} (hi : i < L.length) :
list.drop i (list.take (i + 1) L) = [L.nth_le i hi]

Taking only the first i+1 elements in a list, and then dropping the first i ones, one is left with a list of length 1 made of the i-th element of the original list.

source
theorem list.drop_take_succ_join_eq_nth_le {α : Type u_1} (L : list (list α)) {i : ℕ} (hi : i < L.length) :
list.drop (list.take i (list.map list.length L)).sum (list.take (list.take (i + 1) (list.map list.length L)).sum L.join) = L.nth_le i hi

In a join of sublists, taking the slice between the indices A and B - 1 gives back the original sublist of index i if A is the sum of the lenghts of sublists of index < i, and B is the sum of the lengths of sublists of index ≤ i.

source
theorem list.sum_take_map_length_lt1 {α : Type u_1} (L : list (list α)) {i j : ℕ} (hi : i < L.length) (hj : j < (L.nth_le i hi).length) :
(list.take i (list.map list.length L)).sum + j < (list.take (i + 1) (list.map list.length L)).sum

Auxiliary lemma to control elements in a join.

source
theorem list.sum_take_map_length_lt2 {α : Type u_1} (L : list (list α)) {i j : ℕ} (hi : i < L.length) (hj : j < (L.nth_le i hi).length) :
(list.take i (list.map list.length L)).sum + j < L.join.length

Auxiliary lemma to control elements in a join.

source
theorem list.nth_le_join {α : Type u_1} (L : list (list α)) {i j : ℕ} (hi : i < L.length) (hj : j < (L.nth_le i hi).length) :
L.join.nth_le ((list.take i (list.map list.length L)).sum + j) _ = (L.nth_le i hi).nth_le j hj

The n-th element in a join of sublists is the j-th element of the ith sublist, where n can be obtained in terms of i and j by adding the lengths of all the sublists of index < i, and adding j.

source
theorem list.eq_iff_join_eq {α : Type u_1} (L L' : list (list α)) :
L = L' ↔ L.join = L'.join ∧ list.map list.length L = list.map list.length L'

Two lists of sublists are equal iff their joins coincide, as well as the lengths of the sublists.

source
theorem list.join_drop_length_sub_one {α : Type u_1} {L : list (list α)} (h : L ≠ list.nil) :
(list.drop (L.length - 1) L).join = L.last h
source
theorem list.append_join_map_append {α : Type u_1} (L : list (list α)) (x : list α) :
x ++ (list.map (λ (l : list α), l ++ x) L).join = (list.map (λ (l : list α), x ++ l) L).join ++ x

We can rebracket x ++ (l₁ ++ x) ++ (l₂ ++ x) ++ ... ++ (lₙ ++ x) to (x ++ l₁) ++ (x ++ l₂) ++ ... ++ (x ++ lₙ) ++ x where L = [l₁, l₂, ..., lₙ].

source
theorem list.reverse_join {α : Type u_1} (L : list (list α)) :
L.join.reverse = (list.map list.reverse L).reverse.join

Reversing a join is the same as reversing the order of parts and reversing all parts.

source
theorem list.join_reverse {α : Type u_1} (L : list (list α)) :
L.reverse.join = (list.map list.reverse L).join.reverse

Joining a reverse is the same as reversing all parts and reversing the joined result.