English
If two vectors x and y are on the same ray, then for any nonnegative scalar a, a·x and y are on the same ray.
Русский
Если x и y лежат на одном луче, то для любого неотрицательного a вектор a·x и y лежат на одном луче.
LaTeX
$$$ \operatorname{SameRay}(R, x, y) \;\Rightarrow\; 0 \le a \;\Rightarrow\; \operatorname{SameRay}(R, a \cdot x, y). $$$
Lean4
/-- A nonnegative multiple of a vector is in the same ray as one it is in the same ray as. -/
theorem nonneg_smul_left (h : SameRay R x y) (ha : 0 ≤ a) : SameRay R (a • x) y :=
(h.symm.nonneg_smul_right ha).symm