sameRay_vsub_left — Mathlib

English

If w lies strictly between x and z, then the two consecutive edge vectors y−x and z−y are in the same ray.

Русский

Если w лежит строго между x и z, то вектора y−x и z−y идут вдоль одного луча.

LaTeX

$$Wbtw(R,x,y,z) → SameRay(R, y - x, z - y)$$

Lean4

theorem sameRay_vsub_left {x y z : P} (h : Wbtw R x y z) : SameRay R (y -ᵥ x) (z -ᵥ x) :=
  by
  rcases h with ⟨t, ⟨ht0, _⟩, rfl⟩
  simpa [lineMap_apply] using SameRay.sameRay_nonneg_smul_left (z -ᵥ x) ht0

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