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 α) : [l].join = l

@[simp]

theorem List.join_eq_nil {α : Type u_1} {L : List (List α)} : L.join = [] ↔ ∀ (l : List α), l ∈ L → l = []

@[simp]

theorem List.join_append {α : Type u_1} (L₁ : List (List α)) (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_not_isEmpty {α : Type u_1} {L : List (List α)} : (List.filter (fun (l : List α) => !l.isEmpty) L).join = L.join

@[deprecated List.join_filter_not_isEmpty]

theorem List.join_filter_isEmpty_eq_false {α : Type u_1} {L : List (List α)} : (List.filter (fun (l : List α) => !l.isEmpty) L).join = L.join

Alias of List.join_filter_not_isEmpty.

@[simp]

theorem List.join_filter_ne_nil {α : Type u_1} [DecidablePred fun (l : List α) => l ≠ []] {L : List (List α)} : (List.filter (fun (l : List α) => decide (l ≠ [])) L).join = L.join

theorem List.join_join {α : Type u_1} (l : List (List (List α))) : l.join.join = (List.map List.join l).join

theorem List.length_join' {α : Type u_1} (L : List (List α)) : L.join.length = Nat.sum (List.map List.length L)

See List.length_join for the corresponding statement using List.sum.

theorem List.countP_join' {α : Type u_1} (p : α → Bool) (L : List (List α)) : List.countP p L.join = Nat.sum (List.map (List.countP p) L)

See List.countP_join for the corresponding statement using List.sum.

theorem List.count_join' {α : Type u_1} [BEq α] (L : List (List α)) (a : α) : List.count a L.join = Nat.sum (List.map (List.count a) L)

See List.count_join for the corresponding statement using List.sum.

theorem List.length_bind' {α : Type u_1} {β : Type u_2} (l : List α) (f : α → List β) : (l.bind f).length = Nat.sum (List.map (List.length ∘ f) l)

See List.length_bind for the corresponding statement using List.sum.

theorem List.countP_bind' {α : Type u_1} {β : Type u_2} (p : β → Bool) (l : List α) (f : α → List β) : List.countP p (l.bind f) = Nat.sum (List.map (List.countP p ∘ f) l)

See List.countP_bind for the corresponding statement using List.sum.

theorem List.count_bind' {α : Type u_1} {β : Type u_2} [BEq β] (l : List α) (f : α → List β) (x : β) : List.count x (l.bind f) = Nat.sum (List.map (List.count x ∘ f) l)

See List.count_bind for the corresponding statement using List.sum.

@[simp]

theorem List.bind_eq_nil {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} : l.bind f = [] ↔ ∀ (x : α), x ∈ l → f x = []

theorem List.take_sum_join' {α : Type u_1} (L : List (List α)) (i : ℕ) : List.take (Nat.sum (List.take i (List.map List.length L))) 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.

See List.take_sum_join for the corresponding statement using List.sum.

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

See List.drop_sum_join for the corresponding statement using List.sum.

theorem List.drop_take_succ_eq_cons_getElem {α : Type u_1} (L : List α) (i : ℕ) (h : i < L.length) : List.drop i (List.take (i + 1) L) = [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_getElem]

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

@[deprecated List.drop_take_succ_eq_cons_get]

theorem List.drop_take_succ_eq_cons_nthLe {α : Type u_1} (L : List α) {i : ℕ} (hi : i < L.length) : List.drop i (List.take (i + 1) L) = [L.nthLe 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_getElem' {α : Type u_1} (L : List (List α)) (i : ℕ) (h : i < L.length) : List.drop (Nat.sum (List.take i (List.map List.length L))) (List.take (Nat.sum (List.take (i + 1) (List.map List.length L))) L.join) = 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.

See List.drop_take_succ_join_eq_getElem for the corresponding statement using List.sum.

@[deprecated List.drop_take_succ_join_eq_getElem']

theorem List.drop_take_succ_join_eq_get' {α : Type u_1} (L : List (List α)) (i : Fin L.length) : List.drop (Nat.sum (List.take (↑i) (List.map List.length L))) (List.take (Nat.sum (List.take (↑i + 1) (List.map List.length L))) L.join) = L.get i

theorem List.eq_iff_join_eq {α : Type u_1} (L : List (List α)) (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.

theorem List.join_drop_length_sub_one {α : Type u_1} {L : List (List α)} (h : L ≠ []) : (List.drop (L.length - 1) L).join = L.getLast h

theorem List.append_join_map_append {α : Type u_1} (L : List (List α)) (x : List α) : x ++ (List.map (fun (x_1 : List α) => x_1 ++ x) L).join = (List.map (fun (x_1 : List α) => x ++ x_1) 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 α)) : 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.

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.

theorem List.sublist_join {α : Type u_1} (L : List (List α)) {s : List α} (hs : s ∈ L) : s.Sublist L.join

Any member of L : List (List α)) is a sublist of L.join