Join of a list of lists

This file proves basic properties of List.flatten, which concatenates a list of lists. It is defined in Init.Data.List.Basic.

theorem List.Sublist.flatten {α : Type u_1} {l₁ l₂ : List (List α)} (h : l₁.Sublist l₂) : l₁.flatten.Sublist l₂.flatten

theorem List.Sublist.flatMap {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} (h : l₁.Sublist l₂) (f : α → List β) : (flatMap f l₁).Sublist (flatMap f l₂)

@[deprecated List.length_flatten (since := "2024-10-17")]

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

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

@[deprecated List.length_flatten' (since := "2024-10-25")]

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

Alias of List.length_flatten'.

---

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

@[deprecated List.countP_flatten (since := "2024-10-17")]

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

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

@[deprecated List.countP_flatten' (since := "2024-10-25")]

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

Alias of List.countP_flatten'.

---

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

@[deprecated List.count_flatten (since := "2024-10-17")]

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

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

@[deprecated List.count_flatten' (since := "2024-10-25")]

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

Alias of List.count_flatten'.

---

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

@[deprecated "Use `List.length_flatMap`." (since := "2024-10-17")]

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

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

@[deprecated List.length_flatMap' (since := "2024-10-16")]

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

Alias of List.length_flatMap'.

---

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

@[deprecated "Use `List.countP_flatMap`." (since := "2024-10-17")]

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

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

@[deprecated List.countP_flatMap' (since := "2024-10-16")]

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

Alias of List.countP_flatMap'.

---

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

@[deprecated "Use `List.count_flatMap`." (since := "2024-10-17")]

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

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

@[deprecated List.count_flatMap' (since := "2024-10-16")]

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

Alias of List.count_flatMap'.

---

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

@[deprecated "Use `List.take_sum_flatten`." (since := "2024-10-17")]

theorem List.take_sum_flatten' {α : Type u_1} (L : List (List α)) (i : ℕ) : take (Nat.sum (take i (map length L))) L.flatten = (take i L).flatten

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_flatten for the corresponding statement using List.sum.

@[deprecated List.take_sum_flatten' (since := "2024-10-25")]

theorem List.take_sum_join' {α : Type u_1} (L : List (List α)) (i : ℕ) : take (Nat.sum (take i (map length L))) L.flatten = (take i L).flatten

Alias of List.take_sum_flatten'.

---

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_flatten for the corresponding statement using List.sum.

@[deprecated "Use `List.drop_sum_flatten`." (since := "2024-10-17")]

theorem List.drop_sum_flatten' {α : Type u_1} (L : List (List α)) (i : ℕ) : drop (Nat.sum (take i (map length L))) L.flatten = (drop i L).flatten

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_flatten for the corresponding statement using List.sum.

@[deprecated List.drop_sum_flatten' (since := "2024-10-25")]

theorem List.drop_sum_join' {α : Type u_1} (L : List (List α)) (i : ℕ) : drop (Nat.sum (take i (map length L))) L.flatten = (drop i L).flatten

Alias of List.drop_sum_flatten'.

---

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_flatten 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) : drop i (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 "Use `List.drop_take_succ_flatten_eq_getElem`." (since := "2024-10-17")]

theorem List.drop_take_succ_flatten_eq_getElem' {α : Type u_1} (L : List (List α)) (i : ℕ) (h : i < L.length) : drop (Nat.sum (take i (map length L))) (take (Nat.sum (take (i + 1) (map length L))) L.flatten) = L[i]

In a flatten 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_flatten_eq_getElem for the corresponding statement using List.sum.

@[deprecated List.drop_take_succ_flatten_eq_getElem' (since := "2024-10-15")]

theorem List.drop_take_succ_join_eq_getElem' {α : Type u_1} (L : List (List α)) (i : ℕ) (h : i < L.length) : drop (Nat.sum (take i (map length L))) (take (Nat.sum (take (i + 1) (map length L))) L.flatten) = L[i]

Alias of List.drop_take_succ_flatten_eq_getElem'.

---

In a flatten 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_flatten_eq_getElem for the corresponding statement using List.sum.

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

@[deprecated List.flatten_drop_length_sub_one (since := "2024-10-15")]

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

Alias of List.flatten_drop_length_sub_one.

theorem List.append_flatten_map_append {α : Type u_1} (L : List (List α)) (x : List α) : x ++ (map (fun (x_1 : List α) => x_1 ++ x) L).flatten = (map (fun (x_1 : List α) => x ++ x_1) L).flatten ++ x

We can rebracket x ++ (l₁ ++ x) ++ (l₂ ++ x) ++ ... ++ (lₙ ++ x) to (x ++ l₁) ++ (x ++ l₂) ++ ... ++ (x ++ lₙ) ++ x where L = [l₁, l₂, ..., lₙ].

@[deprecated List.append_flatten_map_append (since := "2024-10-15")]

theorem List.append_join_map_append {α : Type u_1} (L : List (List α)) (x : List α) : x ++ (map (fun (x_1 : List α) => x_1 ++ x) L).flatten = (map (fun (x_1 : List α) => x ++ x_1) L).flatten ++ x

Alias of List.append_flatten_map_append.

---

We can rebracket x ++ (l₁ ++ x) ++ (l₂ ++ x) ++ ... ++ (lₙ ++ x) to (x ++ l₁) ++ (x ++ l₂) ++ ... ++ (x ++ lₙ) ++ x where L = [l₁, l₂, ..., lₙ].