sameRay_vsub — Mathlib

English

If wbtw holds, then the vectors from x to y and from x to z lie on the same ray.

Русский

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

LaTeX

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

Lean4

theorem sameRay_vsub {x y z : P} (h : Wbtw R x y z) : SameRay R (y -ᵥ x) (z -ᵥ y) :=
  by
  rcases h with ⟨t, ⟨ht0, ht1⟩, rfl⟩
  simp_rw [lineMap_apply]
  rcases ht0.lt_or_eq with (ht0' | rfl); swap; · simp
  rcases ht1.lt_or_eq with (ht1' | rfl); swap; · simp
  refine Or.inr (Or.inr ⟨1 - t, t, sub_pos.2 ht1', ht0', ?_⟩)
  simp only [vadd_vsub, smul_smul, vsub_vadd_eq_vsub_sub, smul_sub, ← sub_smul]
  ring_nf

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