# Documentation

Mathlib.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 Init.Data.List.Basic.

theorem List.join_singleton {α : Type u_1} (l : List α) :
List.join [l] = l
@[simp]
theorem List.join_eq_nil {α : Type u_1} {L : List (List α)} :
= [] ∀ (l : List α), l Ll = []
@[simp]
theorem List.join_append {α : Type u_1} (L₁ : List (List α)) (L₂ : List (List α)) :
List.join (L₁ ++ L₂) = ++
theorem List.join_concat {α : Type u_1} (L : List (List α)) (l : List α) :
@[simp]
theorem List.join_filter_isEmpty_eq_false {α : Type u_1} [DecidablePred fun l => ] {L : List (List α)} :
List.join (List.filter (fun l => decide ()) L) =
@[simp]
theorem List.join_filter_ne_nil {α : Type u_1} [DecidablePred fun l => l []] {L : List (List α)} :
List.join (List.filter (fun l => decide (l [])) L) =
theorem List.join_join {α : Type u_1} (l : List (List (List α))) :
= List.join (List.map List.join l)
@[simp]
theorem List.length_join {α : Type u_1} (L : List (List α)) :
= List.sum (List.map List.length L)
@[simp]
theorem List.length_bind {α : Type u_1} {β : Type u_2} (l : List α) (f : αList β) :
List.length () = List.sum (List.map (List.length f) l)
@[simp]
theorem List.bind_eq_nil {α : Type u_1} {β : Type u_2} {l : List α} {f : αList β} :
= [] ∀ (x : α), x lf x = []
theorem List.take_sum_join {α : Type u_1} (L : List (List α)) (i : ) :
List.take (List.sum (List.take i (List.map List.length L))) () = List.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.

theorem List.drop_sum_join {α : Type u_1} (L : List (List α)) (i : ) :
List.drop (List.sum (List.take i (List.map List.length L))) () = List.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.

theorem List.drop_take_succ_eq_cons_get {α : Type u_1} (L : List α) (i : Fin ()) :
List.drop (i) (List.take (i + 1) L) = [List.get L i]

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.

@[deprecated List.drop_take_succ_eq_cons_get]
theorem List.drop_take_succ_eq_cons_nthLe {α : Type u_1} (L : List α) {i : } (hi : i < ) :
List.drop i (List.take (i + 1) L) = [List.nthLe L 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_get {α : Type u_1} (L : List (List α)) (i : Fin ()) :
List.drop (List.sum (List.take (i) (List.map List.length L))) (List.take (List.sum (List.take (i + 1) (List.map List.length L))) ()) = List.get L i

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 lengths of sublists of index < i, and B is the sum of the lengths of sublists of index ≤ i.

@[deprecated List.drop_take_succ_join_eq_get]
theorem List.drop_take_succ_join_eq_nthLe {α : Type u_1} (L : List (List α)) {i : } (hi : i < ) :
List.drop (List.sum (List.take i (List.map List.length L))) (List.take (List.sum (List.take (i + 1) (List.map List.length L))) ()) = List.nthLe L 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 lengths of sublists of index < i, and B is the sum of the lengths of sublists of index ≤ i.

@[deprecated]
theorem List.sum_take_map_length_lt1 {α : Type u_1} (L : List (List α)) {i : } {j : } (hi : i < ) (hj : j < List.length (List.nthLe L i hi)) :
List.sum (List.take i (List.map List.length L)) + j < List.sum (List.take (i + 1) (List.map List.length L))

Auxiliary lemma to control elements in a join.

@[deprecated]
theorem List.sum_take_map_length_lt2 {α : Type u_1} (L : List (List α)) {i : } {j : } (hi : i < ) (hj : j < List.length (List.nthLe L i hi)) :
List.sum (List.take i (List.map List.length L)) + j <

Auxiliary lemma to control elements in a join.

@[deprecated]
theorem List.nthLe_join {α : Type u_1} (L : List (List α)) {i : } {j : } (hi : i < ) (hj : j < List.length (List.nthLe L i hi)) :
List.nthLe () (List.sum (List.take i (List.map List.length L)) + j) (_ : List.sum (List.take i (List.map List.length L)) + j < ) = List.nthLe (List.nthLe L i hi) 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 : List (List α)) (L' : List (List α)) :
L = L' = 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.

theorem List.join_drop_length_sub_one {α : Type u_1} {L : List (List α)} (h : L []) :
theorem List.append_join_map_append {α : Type u_1} (L : List (List α)) (x : List α) :
x ++ List.join (List.map (fun l => l ++ x) L) = List.join (List.map (fun l => x ++ l) L) ++ 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 α)) :
= List.join (List.reverse (List.map List.reverse L))

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 α)) :
= List.reverse (List.join (List.map List.reverse L))

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