ray_eq_iff — Mathlib

English

Two nonzero vectors define the same ray if and only if they lie on the same ray.

Русский

Два ненулевых вектора задают одинаковый луч тогда и только тогда, когда они лежат на одном луче.

LaTeX

$$$ \operatorname{rayOfNeZero}(R, v_1, v_1\neq 0) = \operatorname{rayOfNeZero}(R, v_2, v_2\neq 0) \iff \operatorname{SameRay}(R, v_1, v_2). $$$

Lean4

/-- The rays given by two nonzero vectors are equal if and only if those vectors
satisfy `SameRay`. -/
theorem ray_eq_iff {v₁ v₂ : M} (hv₁ : v₁ ≠ 0) (hv₂ : v₂ ≠ 0) :
    rayOfNeZero R _ hv₁ = rayOfNeZero R _ hv₂ ↔ SameRay R v₁ v₂ :=
  Quotient.eq'

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