not_sameRay_iff_norm_add_lt — Mathlib

English

If x and y are not in the same ray, then |∥x∥ − ∥y∥| < ∥x−y∥.

Русский

Если x и y не лежат на одном луче, то |∥x∥ − ∥y∥| < ∥x−y∥.

LaTeX

$$$\lnot \mathrm{SameRay}(x,y) \Rightarrow |\|x\| - \|y\| | < \|x - y\|.$$$

Lean4

/-- In a strictly convex space, two vectors `x`, `y` are not in the same ray if and only if the
triangle inequality for `x` and `y` is strict. -/
theorem not_sameRay_iff_norm_add_lt : ¬SameRay ℝ x y ↔ ‖x + y‖ < ‖x‖ + ‖y‖ :=
  sameRay_iff_norm_add.not.trans (norm_add_le _ _).lt_iff_ne.symm

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