norm_injOn_ray_right — Mathlib

English

For a nonzero y, the map x ↦ ‖x‖ is injective on the set of x with SameRay x y.

Русский

Для ненулевого y отображение x ↦ ‖x‖ инъективно на множестве x, лежащих на одном луче с y.

LaTeX

$$$$ \text{If } y \neq 0, \{x \mid \text{SameRay}(x,y)\}.\text{InjOn}(\|\cdot\|). $$$$

Lean4

theorem norm_injOn_ray_right (hy : y ≠ 0) : {x | SameRay ℝ x y}.InjOn norm := by
  simpa only [SameRay.sameRay_comm] using norm_injOn_ray_left hy

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