English
If two vectors x and y lie on the same ray, then for every nonnegative scalar a, x and a·y lie on the same ray.
Русский
Если два вектора x и y принадлежат одному и тому же лучу, то для любого неотрицательного скаляра a векторы x и a·y лежат на одном луче.
LaTeX
$$$ \operatorname{SameRay}(R, x, y) \;\Rightarrow\; 0 \le a \;\Rightarrow\; \operatorname{SameRay}(R, x, a \cdot y). $$$
Lean4
/-- A vector is in the same ray as a nonnegative multiple of one it is in the same ray as. -/
theorem nonneg_smul_right (h : SameRay R x y) (ha : 0 ≤ a) : SameRay R x (a • y) :=
h.trans (sameRay_nonneg_smul_right y ha) fun hy => Or.inr <| by rw [hy, smul_zero]