wbtw_const_vadd_iff — Mathlib

English

Applying a constant translation v to all points preserves Wbtw: Wbtw R (v + x) (v + y) (v + z) is equivalent to Wbtw R x y z.

Русский

При прибавлении константы v ко всем точкам сохраняется Wbtw: Wbtw R (v + x) (v + y) (v + z) эквивалентно Wbtw R x y z.

LaTeX

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

Lean4

@[simp]
theorem wbtw_const_vadd_iff {x y z : P} (v : V) : Wbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ↔ Wbtw R x y z :=
  mem_const_vadd_affineSegment _

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