English
There is a natural equivalence relation on the nonzero ray vectors, equating two vectors if they lie on the same ray.
Русский
Существет естественное эквивалентное отношения на непустых лучевых векторах, причём два вектора эквивалентны, если они лежат на одном луче.
LaTeX
$$$\text{Setoid}(\text{RayVector } R M)\;:\; r(x,y) := \operatorname{SameRay}(R, x, y).$$$
Lean4
/-- The setoid of the `SameRay` relation for the subtype of nonzero vectors. -/
instance Setoid : Setoid (RayVector R M) where
r x y := SameRay R (x : M) y
iseqv :=
⟨fun _ => SameRay.refl _, fun h => h.symm, by
intro x y z hxy hyz
exact hxy.trans hyz fun hy => (y.2 hy).elim⟩
