English
Two vectors x,y are on the same ray iff either one is zero or the unit vectors are equal.
Русский
Два вектора лежат на одной луче тогда и только тогда, когда один из них нулевой или единичные векторы равны.
LaTeX
$$$$ \text{SameRay}(x,y) \iff x=0 \lor y=0 \lor \|x\|^{-1}x = \|y\|^{-1}y. $$$$
Lean4
/-- Two vectors `x y` in a real normed space are on the ray if and only if one of them is zero or
the unit vectors `‖x‖⁻¹ • x` and `‖y‖⁻¹ • y` are equal. -/
theorem sameRay_iff_inv_norm_smul_eq : SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y :=
by
rcases eq_or_ne x 0 with (rfl | hx); · simp [SameRay.zero_left]
rcases eq_or_ne y 0 with (rfl | hy); · simp [SameRay.zero_right]
simp only [sameRay_iff_inv_norm_smul_eq_of_ne hx hy, *, false_or]
