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.

@[simp]
theorem list.join_nil {α : Type u_1} :
@[simp]
theorem list.join_eq_nil {α : Type u_1} {L : list (list α)} :
L.join = list.nil ∀ (l : list α), l Ll = list.nil
@[simp]
theorem list.join_append {α : Type u_1} (L₁ L₂ : list (list α)) :
(L₁ ++ L₂).join = L₁.join ++ L₂.join
@[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
@[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 lf 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.