English
For any p1, p2, p3, p4, the list [p1, p2, p3, p4] has the Wbtw relation with respect to R iff the four triplewise conditions hold: Wbtw(p1,p2,p3), Wbtw(p1,p2,p4), Wbtw(p1,p3,p4), and Wbtw(p2,p3,p4).
Русский
Для p1, p2, p3, p4 список [p1, p2, p3, p4] удовлетворяет Wbtw по R тогда и только тогда, когда выполняются четыре условий: Wbtw(p1,p2,p3), Wbtw(p1,p2,p4), Wbtw(p1,p3,p4), Wbtw(p2,p3,p4).
LaTeX
$$$Wbtw(R,[p_1,p_2,p_3,p_4]) \\iff Wbtw(R,p_1,p_2,p_3) \\land Wbtw(R,p_1,p_2,p_4) \\land Wbtw(R,p_1,p_3,p_4) \\land Wbtw(R,p_2,p_3,p_4)$$$
Lean4
theorem wbtw_four {p₁ p₂ p₃ p₄ : P} :
[p₁, p₂, p₃, p₄].Wbtw R ↔ Wbtw R p₁ p₂ p₃ ∧ Wbtw R p₁ p₂ p₄ ∧ Wbtw R p₁ p₃ p₄ ∧ Wbtw R p₂ p₃ p₄ := by
simp [List.Wbtw, triplewise_cons, and_assoc]
