sameRay_neg_smul_left_iff — Mathlib

English

For any v and r, the vectors r·v and −v are on the same ray precisely when r < 0, assuming the scalars and vectors are nonzero as needed.

Русский

Для любых v и r векторы r·v и −v лежат в одном луче тогда и только тогда, когда r < 0 (при нужных условиях ненулевости).

LaTeX

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

Lean4

@[simp]
theorem sameRay_neg_smul_left_iff {v : M} {r : R} : SameRay R (r • v) (-v) ↔ r ≤ 0 ∨ v = 0 :=
  SameRay.sameRay_comm.trans sameRay_neg_smul_right_iff

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