norm_injOn_ray_left — Mathlib

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]

Похожие утверждения