Refining List.splitBy #
Mathlib/Data/List/SplitBy.lean characterizes List.splitBy (List.splitBy_eq_iff) but has no
lemma comparing the splittings by two relations. When r implies s, every run of r lies in a
run of s, so splitting by s and then splitting each run by r splits by r. [UPSTREAM]
candidate for that file.
Main results #
List.flatMap_splitBy_splitBy: splitting by a coarser relation and then by a finer one splits by the finer one.
theorem
List.flatMap_splitBy_splitBy
{α : Type u_1}
{r s : α → α → Bool}
(h : ∀ (x y : α), r x y = true → s x y = true)
(l : List α)
:
flatMap (splitBy r) (splitBy s l) = splitBy r l
Splitting by a coarser relation and then by a finer one splits by the finer one.