sameRay_smul_left_iff — Mathlib

English

Let v be any vector in M and r any scalar in R. The vectors r·v and v lie on the same ray if and only if either r is nonnegative or v is the zero vector.

Русский

Пусть v — произвольный вектор в M, a скаляр r — элемент поля R. Векторы r·v и v лежат в одном луче тогда и только тогда, когда либо r неотрицательно, либо v = 0.

LaTeX

$$$\operatorname{SameRay}(r\cdot v, v) \iff 0 \le r \lor v = 0$$$

Lean4

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

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