sameRay_vsub_right — Mathlib

English

If x, y, z satisfy weak betweenness, then the second difference vector from z to x and from z to y are in the same ray.

Русский

Если x, y, z удовлетворяют слабому betw, то вектора z−x и z−y лежат в одном луче.

LaTeX

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

Lean4

theorem sameRay_vsub_right {x y z : P} (h : Wbtw R x y z) : SameRay R (z -ᵥ x) (z -ᵥ y) :=
  by
  rcases h with ⟨t, ⟨_, ht1⟩, rfl⟩
  simpa [lineMap_apply, vsub_vadd_eq_vsub_sub, sub_smul] using
    SameRay.sameRay_nonneg_smul_right (z -ᵥ x) (sub_nonneg.2 ht1)

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