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