English
The SameRay relation is symmetric: If x is on the same ray as y, then y is on the same ray as x.
Русский
Отношение SameRay симметрично: если x лежит на той же луче, что и y, то y лежит на той же луче, что и x.
LaTeX
$$$\\text{SameRay}\\,R\\,x\\,y \\iff \\text{SameRay}\\,R\\,y\\,x$$$
Lean4
/-- Two vectors are in the same ray if either one of them is zero or some positive multiples of them
are equal (in the typical case over a field, this means one of them is a nonnegative multiple of
the other). -/
@[nolint unusedArguments]
def SameRay (R : Type*) [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type*} [AddCommMonoid M]
[Module R M] (v₁ v₂ : M) : Prop :=
v₁ = 0 ∨ v₂ = 0 ∨ ∃ r₁ r₂ : R, 0 < r₁ ∧ 0 < r₂ ∧ r₁ • v₁ = r₂ • v₂
