sameRay_smul_left_iff_of_ne — Mathlib

English

If v ≠ 0 and r ≠ 0, then the vectors r·v and v lie on the same ray if and only if r is positive.

Русский

Если v ≠ 0 и r ≠ 0, то векторы r·v и v лежат в одном луче тогда и только тогда, когда r > 0.

LaTeX

$$$\operatorname{SameRay}(r\cdot v, v) \iff 0 < r$ assuming $v \neq 0$ and $r \neq 0$$$

Lean4

/-- A multiple of a nonzero vector is in the same ray as that vector if and only if that multiple
is positive. -/
theorem sameRay_smul_left_iff_of_ne {v : M} (hv : v ≠ 0) {r : R} (hr : r ≠ 0) : SameRay R (r • v) v ↔ 0 < r :=
  SameRay.sameRay_comm.trans (sameRay_smul_right_iff_of_ne hv hr)

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