English
If two vectors lie on the same ray, their images under a linear map also lie on the same ray.
Русский
Если два вектора лежат на одном луче, их изображения под линейным отображением также лежат на одном луче.
LaTeX
$$$ \operatorname{SameRay}(R, x, y) \Rightarrow \operatorname{SameRay}(R, f(x), f(y)) $$$
Lean4
/-- If two vectors are on the same ray then they remain so after applying a linear map. -/
theorem map (f : M →ₗ[R] N) (h : SameRay R x y) : SameRay R (f x) (f y) :=
(h.imp fun hx => by rw [hx, map_zero]) <|
Or.imp (fun hy => by rw [hy, map_zero]) fun ⟨r₁, r₂, hr₁, hr₂, h⟩ =>
⟨r₁, r₂, hr₁, hr₂, by rw [← f.map_smul, ← f.map_smul, h]⟩
