English
A triple x, y, z satisfies Wbtw_R(x,y,z) exactly when the vectors y−x and z−y are on the same ray, i.e., SameRay_R(y−x, z−y).
Русский
Тройка x, y, z образует между, если и только если векторы y−x и z−y лежат на одном луче: SameRay_R(y−x, z−y).
LaTeX
$$$Wbtw_R(x,y,z) \iff SameRay_R (y -\! x) (z -\! y)$$$
Lean4
theorem wbtw_iff_sameRay_vsub {x y z : P} : Wbtw R x y z ↔ SameRay R (y -ᵥ x) (z -ᵥ y) :=
by
refine ⟨Wbtw.sameRay_vsub, fun h => ?_⟩
rcases h with (h | h | ⟨r₁, r₂, hr₁, hr₂, h⟩)
· rw [vsub_eq_zero_iff_eq] at h
simp [h]
· rw [vsub_eq_zero_iff_eq] at h
simp [h]
· refine
⟨r₂ / (r₁ + r₂),
⟨div_nonneg hr₂.le (add_nonneg hr₁.le hr₂.le),
div_le_one_of_le₀ (le_add_of_nonneg_left hr₁.le) (add_nonneg hr₁.le hr₂.le)⟩,
?_⟩
have h' : z = r₂⁻¹ • r₁ • (y -ᵥ x) +ᵥ y := by simp [h, hr₂.ne']
rw [eq_comm]
simp only [lineMap_apply, h', vadd_vsub_assoc, smul_smul, ← add_smul, eq_vadd_iff_vsub_eq, smul_add]
convert (one_smul R (y -ᵥ x)).symm
field_simp
