eq_of_norm_eq_of_norm_add_eq — Mathlib

English

Two vectors are not on the same ray if and only if the triangle inequality is strict: ∥x+y∥ < ∥x∥ + ∥y∥.

Русский

Два вектора не лежат на одном луче тогда и только тогда, когда неострогива треугольного неравенства: ∥x+y∥ < ∥x∥ + ∥y∥.

LaTeX

$$$\neg \mathrm{SameRay}(x,y) \iff \|x+y\| < \|x\| + \|y\|.$$$

Lean4

/-- If `x` and `y` are two vectors in a strictly convex space have the same norm and the norm of
their sum is equal to the sum of their norms, then they are equal. -/
theorem eq_of_norm_eq_of_norm_add_eq (h₁ : ‖x‖ = ‖y‖) (h₂ : ‖x + y‖ = ‖x‖ + ‖y‖) : x = y :=
  (sameRay_iff_norm_add.mpr h₂).eq_of_norm_eq h₁

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