isChain_isInfix — Mathlib

English

For every list l, the relation defined by adjacent elements corresponding to infix occurrences is a chain on l.

Русский

Для любого списка l отношение между соседними элементами, соответствующее вхождениям инфиксирования, образует цепь на l.

LaTeX

$$$IsChain\\;R\\;l$ для связи через IsInfix, формула не развёрнута$$

Lean4

theorem isChain_isInfix : ∀ l : List α, IsChain (fun x y => [x, y] <:+: l) l
  | [] => .nil
  | [_] => .singleton _
  | a :: b :: l => .cons_cons ⟨[], l, by simp⟩ ((isChain_isInfix (b :: l)).imp fun _ _ h => h.trans ⟨[a], [], by simp⟩)

Похожие утверждения