equiv_iff_sameRay — Mathlib

English

For nonzero vectors v1,v2, their rays are equal if and only if v1 and v2 lie on the same ray.

Русский

Для ненулевых векторов v1 и v2 лучи равны тогда и только тогда, когда они лежат на одном луче.

LaTeX

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

Lean4

/-- Equivalence of nonzero vectors, in terms of `SameRay`. -/
theorem equiv_iff_sameRay {v₁ v₂ : RayVector R M} : v₁ ≈ v₂ ↔ SameRay R (v₁ : M) v₂ :=
  Iff.rfl

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