sameRay_iff_norm_add — Mathlib

English

If ∥x∥ = ∥y∥ and ∥x+y∥ = ∥x∥ + ∥y∥, then x = y.

Русский

Если нормы равны и сумма норм равна сумме норм, то векторы совпадают: x = y.

LaTeX

$$$\|x\| = \|y\| \land \|x+y\| = \|x\| + \|y\| \Rightarrow x = y.$$$

Lean4

/-- In a strictly convex space, two vectors `x`, `y` are in the same ray if and only if the triangle
inequality for `x` and `y` becomes an equality. -/
theorem sameRay_iff_norm_add : SameRay ℝ x y ↔ ‖x + y‖ = ‖x‖ + ‖y‖ :=
  ⟨SameRay.norm_add, fun h => Classical.not_not.1 fun h' => (norm_add_lt_of_not_sameRay h').ne h⟩

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