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