Split a list into contiguous runs of elements which pairwise satisfy a relation.

This file provides the basic API for List.splitBy which is defined in Core. The main results are the following:

• List.join_splitBy: the lists in List.splitBy join to the original list.
• List.nil_not_mem_splitBy: the empty list is not contained in List.splitBy.
• List.chain'_of_mem_splitBy: any two adjacent elements in a list in List.splitBy are related by the specified relation.
• List.chain'_getLast_head_splitBy: the last element of each list in List.splitBy is not related to the first element of the next list.

@[simp]

theorem List.splitBy_nil {α : Type u_1} (r : α → α → Bool) : splitBy r [] = []

@[simp]

theorem List.flatten_splitBy {α : Type u_1} (r : α → α → Bool) (l : List α) : (splitBy r l).flatten = l

theorem List.nil_not_mem_splitBy {α : Type u_1} (r : α → α → Bool) (l : List α) : ¬[] ∈ splitBy r l

theorem List.ne_nil_of_mem_splitBy {α : Type u_1} {m : List α} (r : α → α → Bool) {l : List α} (h : m ∈ splitBy r l) : m ≠ []

theorem List.chain'_of_mem_splitBy {α : Type u_1} {m : List α} {r : α → α → Bool} {l : List α} (h : m ∈ splitBy r l) : Chain' (fun (x y : α) => r x y = true) m

theorem List.chain'_getLast_head_splitBy {α : Type u_1} (r : α → α → Bool) (l : List α) : Chain' (fun (a b : List α) => ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (splitBy r l)

@[deprecated List.splitBy_nil (since := "2024-10-30")]

theorem List.groupBy_nil {α : Type u_1} (r : α → α → Bool) : splitBy r [] = []

Alias of List.splitBy_nil.

@[deprecated List.flatten_splitBy (since := "2024-10-30")]

theorem List.flatten_groupBy {α : Type u_1} (r : α → α → Bool) (l : List α) : (splitBy r l).flatten = l

Alias of List.flatten_splitBy.

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

theorem List.join_splitBy {α : Type u_1} (r : α → α → Bool) (l : List α) : (splitBy r l).flatten = l

Alias of List.flatten_splitBy.

@[deprecated List.nil_not_mem_splitBy (since := "2024-10-30")]

theorem List.nil_not_mem_groupBy {α : Type u_1} (r : α → α → Bool) (l : List α) : ¬[] ∈ splitBy r l

Alias of List.nil_not_mem_splitBy.

@[deprecated List.ne_nil_of_mem_splitBy (since := "2024-10-30")]

theorem List.ne_nil_of_mem_groupBy {α : Type u_1} {m : List α} (r : α → α → Bool) {l : List α} (h : m ∈ splitBy r l) : m ≠ []

Alias of List.ne_nil_of_mem_splitBy.

@[deprecated List.chain'_of_mem_splitBy (since := "2024-10-30")]

theorem List.chain'_of_mem_groupBy {α : Type u_1} {m : List α} {r : α → α → Bool} {l : List α} (h : m ∈ splitBy r l) : Chain' (fun (x y : α) => r x y = true) m

Alias of List.chain'_of_mem_splitBy.

@[deprecated List.chain'_getLast_head_splitBy (since := "2024-10-30")]

theorem List.chain'_getLast_head_groupBy {α : Type u_1} (r : α → α → Bool) (l : List α) : Chain' (fun (a b : List α) => ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (splitBy r l)

Alias of List.chain'_getLast_head_splitBy.