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.

@[simp]
theorem list.join_singleton {α : Type u_1} (l : list α) :
[l].join = l
@[simp]
theorem list.join_eq_nil {α : Type u_1} {L : list (list α)} :
L.join = list.nil (l : list α), l L l = list.nil
@[simp]
theorem list.join_append {α : Type u_1} (L₁ L₂ : list (list α)) :
(L₁ ++ L₂).join = L₁.join ++ L₂.join
theorem list.join_concat {α : Type u_1} (L : list (list α)) (l : list α) :
(L.concat l).join = L.join ++ l
@[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
@[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
theorem list.join_join {α : Type u_1} (l : list (list (list α))) :
@[simp]
theorem list.length_join {α : Type u_1} (L : list (list α)) :
@[simp]
theorem list.length_bind {α : Type u_1} {β : Type u_2} (l : list α) (f : α list β) :
@[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
theorem list.take_sum_join {α : Type u_1} (L : list (list α)) (i : ) :

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.

theorem list.drop_sum_join {α : Type u_1} (L : list (list α)) (i : ) :

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.

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.

theorem list.drop_take_succ_join_eq_nth_le {α : Type u_1} (L : list (list α)) {i : } (hi : i < L.length) :

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.

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

Auxiliary lemma to control elements in a join.

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

Auxiliary lemma to control elements in a join.

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.

theorem list.eq_iff_join_eq {α : Type u_1} (L L' : list (list α)) :

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

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
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ₙ].

theorem list.reverse_join {α : Type u_1} (L : list (list α)) :

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

theorem list.join_reverse {α : Type u_1} (L : list (list α)) :

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