wbtw_triple — Mathlib

English

For any p1, p2, p3, the list [p1, p2, p3] has the Wbtw relation with respect to R if and only if the triple p1, p2, p3 satisfies the Wbtw relation.

Русский

Для любых p1, p2, p3 множество [p1, p2, p3] имеет отношение Wbtw по R тогда и только тогда, когда тройка точек удовлетворяет условию Wbtw.

LaTeX

$$$Wbtw(R,[p_1,p_2,p_3]) \\iff Wbtw(R,p_1,p_2,p_3)$$$

Lean4

@[simp]
theorem wbtw_triple {p₁ p₂ p₃ : P} : [p₁, p₂, p₃].Wbtw R ↔ Wbtw R p₁ p₂ p₃ := by simp [List.Wbtw]

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