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_notMem_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

@[deprecated _private.Mathlib.Data.List.SplitBy.0.List.nil_notMem_splitByLoop (since := "2025-05-23")]

theorem List.nil_not_mem_splitByLoop {α : Type u_1} {r : α → α → Bool} {l : List α} {a : α} {g : List α} : ¬[] ∈ splitBy.loop r l a g []

Alias of _private.Mathlib.Data.List.SplitBy.0.List.nil_notMem_splitByLoop.

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

@[deprecated List.nil_notMem_splitBy (since := "2025-05-23")]

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

Alias of List.nil_notMem_splitBy.

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.nil_notMem_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_notMem_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.