sameRay_of_mem_segment — Mathlib

English

If x lies in the segment between y and z, then (x−y) and (z−x) have the same ray relation.

Русский

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

LaTeX

$$$$ x \in [y -[\mathbb{K}] z] \Rightarrow \text{SameRay}_{\mathbb{K}}(x-y,z-x). $$$$

Lean4

theorem sameRay_of_mem_segment [CommRing 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E]
    {x y z : E} (h : x ∈ [y -[𝕜] z]) : SameRay 𝕜 (x - y) (z - x) :=
  by
  rw [segment_eq_image'] at h
  rcases h with ⟨θ, ⟨hθ₀, hθ₁⟩, rfl⟩
  simpa only [add_sub_cancel_left, ← sub_sub, sub_smul, one_smul] using
    (SameRay.sameRay_nonneg_smul_left (z - y) hθ₀).nonneg_smul_right (sub_nonneg.2 hθ₁)

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