English
For a linear equivalence e, SameRay(x, y) is preserved and reflected: x and y are on the same ray after applying e iff they were on the same ray before.
Русский
Для линейного эквивалента e сохранение и отражение лучей: x и y на одном луче после применения e тогда и только тогда, когда они были на одном луче до применения.
LaTeX
$$$ \operatorname{SameRay}(R, e(x), e(y)) \iff \operatorname{SameRay}(R, x, y). $$$
Lean4
/-- The images of two vectors under a linear equivalence are on the same ray if and only if the
original vectors are on the same ray. -/
@[simp]
theorem sameRay_map_iff (e : M ≃ₗ[R] N) : SameRay R (e x) (e y) ↔ SameRay R x y :=
Function.Injective.sameRay_map_iff (EquivLike.injective e)
