English
On a list of points, the property Wbtw holds pairwise along consecutive triples; there is a decomposition into the head and tail conditions.
Русский
Для списка точек свойство Wbtw сохраняется попарно по соседним тройкам, что эквивалентно разбиению на голову и хвост.
LaTeX
$$$(p :: l).Wbtw R \ \Longleftrightarrow\ (l.Pairs) \land l.Wbtw R$$$
Lean4
theorem wbtw_cons {p : P} {l : List P} : (p :: l).Wbtw R ↔ l.Pairwise (Wbtw R p) ∧ l.Wbtw R :=
triplewise_cons