eq_of_norm_eq — Mathlib

English

If two points x,y are on the same ray and have equal norms, then x = y.

Русский

Если два вектора лежат на одном луче и имеют равные нормы, то они равны.

LaTeX

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

Lean4

/-- If two points on the same ray have the same norm, then they are equal. -/
theorem eq_of_norm_eq (h : SameRay ℝ x y) (hn : ‖x‖ = ‖y‖) : x = y :=
  (sameRay_iff_of_norm_eq hn).mp h

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