English
Let p be a point on the affine space P. For any x, y, z ∈ P, the relation Sbtw R (x −ᵥ p) (y −ᵥ p) (z −ᵥ p) holds if and only if Sbtw R x y z holds. Translation by a fixed base point preserves the Sbtw relation.
Русский
Пусть p — точка аффинного пространства P. Для любых x, y, z ∈ P выполняется, что Sbtw R (x −ᵥ p) (y −ᵥ p) (z −ᵥ p) эквивалентно Sbtw R x y z. Перемещение базовой точки сохраняет отношение Sbtw.
LaTeX
$$$Sbtw R (x -\!\!\! v p) (y -\!\!\! v p) (z -\!\!\! v p) \iff Sbtw R x y z$$$
Lean4
@[simp]
theorem sbtw_vsub_const_iff {x y z : P} (p : P) : Sbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ↔ Sbtw R x y z := by
rw [Sbtw, Sbtw, wbtw_vsub_const_iff, (vsub_left_injective p).ne_iff, (vsub_left_injective p).ne_iff]
