English
Let α be a type and R a relation on α. If l is an R-chain, and R(v, a) holds for the first element a of l whenever l is nonempty, then the concatenation (v, a1, a2, ..., an) is also an R-chain. In particular, extending a chain by a new first element preserves the chain property provided the relation holds with the first element of the original chain.
Русский
Пусть α — множество, R — отношение на α. Если l является R-цепью и если при непустой цепи l выполняется R(v, a1) для первого элемента a1, то добавление v в начало цепи сохраняет свойство быть цепью. То есть (v, a1, a2, ..., an) является R-цепью.
LaTeX
$$$\\forall \\alpha \\forall R:\\alpha \\to \\alpha \\to Prop,\\ \\forall l:\\text{List }\\alpha,\\forall v:\\alpha,\\ hl:\\ IsChain_R(l),\\ hv:(l \\ne \\emptyset \\to R\\, v\\, (\\text{head}(l)))\\,\\Rightarrow\\, IsChain_R(v::l)$$$
Lean4
theorem isChain_cons {α : Type*} {R : α → α → Prop} {l : List α} {v : α} (hl : l.IsChain R)
(hv : (lne : l ≠ []) → R v (l.head lne)) : (v :: l).IsChain R := by cases l <;> grind
