wbtw_vadd_const_iff — Mathlib

English

In a vector space, adding a constant vector p to all three points preserves the weak-between relation: Wbtw R (x + p) (y + p) (z + p) iff Wbtw R x y z.

Русский

Векторное пространство: добавление константного вектора p ко всем трём точкам сохраняет слабое между.

LaTeX

$$Wbtw R (x + p) (y + p) (z + p) \iff Wbtw R x y z$$

Lean4

@[simp]
theorem wbtw_vadd_const_iff {x y z : V} (p : P) : Wbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) ↔ Wbtw R x y z :=
  mem_vadd_const_affineSegment _

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