English
For any p1, p2, p3, the list [p1, p2, p3] has the Sbtw relation with respect to R iff Sbtw(p1, p2, p3) holds.
Русский
Для любых p1, p2, p3 список [p1, p2, p3] удовлетворяет Sbtw по R тогда и только тогда, когда выполняется Sbtw(p1, p2, p3).
LaTeX
$$$Sbtw(R,[p_1,p_2,p_3]) \\iff Sbtw(R,p_1,p_2,p_3)$$$
Lean4
@[simp]
theorem sbtw_triple [IsOrderedRing R] {p₁ p₂ p₃ : P} : [p₁, p₂, p₃].Sbtw R ↔ Sbtw R p₁ p₂ p₃ :=
by
simp only [List.Sbtw, wbtw_triple, ne_eq, pairwise_cons, mem_cons, not_mem_nil, or_false, forall_eq_or_imp, forall_eq,
IsEmpty.forall_iff, implies_true, Pairwise.nil, and_self, and_true]
exact ⟨fun ⟨hw, ⟨h₁₂, h₁₃⟩, h₂₃⟩ ↦ ⟨hw, Ne.symm h₁₂, h₂₃⟩, fun h ↦ ⟨h.1, ⟨h.2.1.symm, h.left_ne_right⟩, h.2.2⟩⟩
