sameRay_neg_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 < 0.

Русский

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

LaTeX

$$$\operatorname{SameRay}(r\cdot v, -v) \iff r < 0$ при $v \neq 0$ и $r \neq 0$$$

Lean4

theorem sameRay_neg_smul_left_iff_of_ne {v : M} {r : R} (hv : v ≠ 0) (hr : r ≠ 0) : SameRay R (r • v) (-v) ↔ r < 0 :=
  SameRay.sameRay_comm.trans <| sameRay_neg_smul_right_iff_of_ne hv hr

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