English
For the pieces produced by splitBy, the chain property across adjacent pieces asserts that the relation between the last element of the first piece and the head of the next piece is false for at least one witness if appropriate.
Русский
Для соседних блоков в splitBy выполняется свойство цепи: существует пара «последний элемент первого блока» и «первый элемент второго блока», для которой отношение r истинно/ложно соответственно.
LaTeX
$$$ (l.splitBy r).IsChain (\\lambda a b, \\exists ha\\exists hb, r (a.getLast ha) (b.head hb) = false) $$$
Lean4
theorem isChain_getLast_head_splitBy (r : α → α → Bool) (l : List α) :
(l.splitBy r).IsChain fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false := by
cases l with
| nil => exact isChain_nil
| cons _ _ =>
apply isChain_getLast_head_splitByLoop _ not_mem_nil isChain_nil
rintro _ ⟨⟩
