English
A list is an R-chain iff for every adjacent pair of positions i, i+1 with i+1 < length, the corresponding elements satisfy R.
Русский
Список является цепью по отношению R тогда и только тогда, когда для всех соседних элементов удовлетворяется R.
LaTeX
$$$\\forall \\{\\alpha\\}, \\forall R:\\, \\alpha \\to \\alpha \\to \\mathrm{Prop}, \\forall l:\\, \\text{List }\\alpha, IsChain\\, R\\, l \\leftrightarrow \\forall i, j, (i+1 < l.length) \\rightarrow R (get l ⟨i, ?\\rangle) (get l ⟨i+1, j\\rangle) $$$
Lean4
theorem isChain_iff_get {R} :
∀ {l : List α}, IsChain R l ↔ ∀ (i : ℕ) (h : i + 1 < l.length), R (get l ⟨i, by cutsat⟩) (get l ⟨i + 1, h⟩) := by
simp [isChain_iff_getElem]
