English
For an injective map f, two vectors have the same ray image under f if and only if the original vectors have the same ray.
Русский
Для инъективного отображения f изображения двух векторов имеют один и тот же луч под f ⇔ сами векторы имеют один и тот же луч.
LaTeX
$$$ \text{If } f \text{ is injective, then } \operatorname{SameRay}(R, f(x), f(y)) \iff \operatorname{SameRay}(R, x, y). $$$
Lean4
/-- The images of two vectors under an injective linear map are on the same ray if and only if the
original vectors are on the same ray. -/
theorem _root_.Function.Injective.sameRay_map_iff {F : Type*} [FunLike F M N] [LinearMapClass F R M N] {f : F}
(hf : Function.Injective f) : SameRay R (f x) (f y) ↔ SameRay R x y := by
simp only [SameRay, map_zero, ← hf.eq_iff, map_smul]
