sameRay_iff_of_norm_eq — Mathlib

English

If x and y are on the same ray, then ‖x‖ = ‖y‖ if and only if x = y.

Русский

Если x и y лежат на одном луче, то ‖x‖ = ‖y‖ тогда и только тогда, когда x = y.

LaTeX

$$$$ \text{SameRay}(\mathbb{R},x,y) \Rightarrow (\|x\| = \|y\|) \Leftrightarrow x = y. $$$$

Lean4

/-- Two vectors of the same norm are on the same ray if and only if they are equal. -/
theorem sameRay_iff_of_norm_eq (h : ‖x‖ = ‖y‖) : SameRay ℝ x y ↔ x = y :=
  by
  obtain rfl | hy := eq_or_ne y 0
  · rw [norm_zero, norm_eq_zero] at h
    exact iff_of_true (SameRay.zero_right _) h
  · exact ⟨fun hxy => norm_injOn_ray_right hy hxy SameRay.rfl h, fun hxy => hxy ▸ SameRay.rfl⟩

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