sameRay_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent

English

If x and y are in the same ray with both x and y nonzero, there exists a positive scalar r such that x = r·y.

Русский

Если x и y лежат в одном луче и оба ненулевые, существует положительный скаляр r такой, что x = r·y.

LaTeX

$$$\exists r>0\; (x= r\cdot y)$ при $\operatorname{SameRay}(x,y)$ и $x,y \neq 0$$$

Lean4

/-- Two vectors are in the same ray, or they are nonzero and the first is in the same ray as the
negation of the second, if and only if they are not linearly independent. -/
theorem sameRay_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent {x y : M} :
    SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y] :=
  by
  rw [← sameRay_or_sameRay_neg_iff_not_linearIndependent]
  by_cases hx : x = 0; · simp [hx]
  by_cases hy : y = 0 <;> simp [hx, hy]

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