norm_eq_iff — Mathlib

English

If x,y are on the same ray, then ‖x‖ = ‖y‖ iff x = y.

Русский

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

LaTeX

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

Lean4

/-- The norms of two vectors on the same ray are equal if and only if they are equal. -/
theorem norm_eq_iff (h : SameRay ℝ x y) : ‖x‖ = ‖y‖ ↔ x = y :=
  ⟨h.eq_of_norm_eq, fun h => h ▸ rfl⟩

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