English
For a nonzero x, the map y ↦ ‖y‖ is injective on the set of y with SameRay x y.
Русский
При x ≠ 0 отображение y ↦ ‖y‖ инъективно на множестве y, таких что x и y лежат на одном луче.
LaTeX
$$$$ \text{If } x \neq 0, \{y \mid \text{SameRay}(x,y)\}.\text{InjOn}(\|\cdot\|). $$$$
Lean4
theorem norm_injOn_ray_left (hx : x ≠ 0) : {y | SameRay ℝ x y}.InjOn norm :=
by
rintro y hy z hz h
rcases hy.exists_nonneg_left hx with ⟨r, hr, rfl⟩
rcases hz.exists_nonneg_left hx with ⟨s, hs, rfl⟩
rw [norm_smul, norm_smul, mul_left_inj' (norm_ne_zero_iff.2 hx), norm_of_nonneg hr, norm_of_nonneg hs] at h
rw [h]