mathlib documentation

data.list.join

Join of a list of lists #

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_nil {α : Type u_1} :
[list.nil].join = list.nil
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
@[simp]
theorem list.join_filter_empty_eq_ff {α : Type u_1} [decidable_pred (λ (l : list α), l.empty = ff)] {L : list (list α)} :
(list.filter (λ (l : list α), l.empty = 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
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.