English
For x, y, z ∈ E, x lies on the segment [y,z] if and only if the vectors (x−y) and (z−x) form the same ray; i.e., SameRay 𝕜 (x−y) (z−x).
Русский
Для любых x, y, z ∈ E точка x принадлежит отрезку [y,z] тогда и только тогда вектора (x−y) и (z−x) образуют один и тот же луч; то есть SameRay 𝕜 (x−y) (z−x).
LaTeX
$$$ x \in [y -[\mathbb{k}] z] \iff \text{SameRay}_{\mathbb{k}}(x-y, z-x) $$$
Lean4
theorem mem_segment_iff_sameRay : x ∈ [y -[𝕜] z] ↔ SameRay 𝕜 (x - y) (z - x) :=
by
refine ⟨sameRay_of_mem_segment, fun h => ?_⟩
rcases h.exists_eq_smul_add with ⟨a, b, ha, hb, hab, hxy, hzx⟩
rw [add_comm, sub_add_sub_cancel] at hxy hzx
rw [← mem_segment_translate _ (-x), neg_add_cancel]
refine ⟨b, a, hb, ha, add_comm a b ▸ hab, ?_⟩
rw [← sub_eq_neg_add, ← neg_sub, hxy, ← sub_eq_neg_add, hzx, smul_neg, smul_comm, neg_add_cancel]
