lt_norm_sub_of_not_sameRay — Mathlib

English

If x and y are not on the same ray, then the difference of norms is strictly less than the norm of the difference: ∥x∥ − ∥y∥ < ∥x−y∥.

Русский

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

LaTeX

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

Lean4

theorem lt_norm_sub_of_not_sameRay (h : ¬SameRay ℝ x y) : ‖x‖ - ‖y‖ < ‖x - y‖ :=
  by
  nth_rw 1 [← sub_add_cancel x y] at h ⊢
  exact sub_lt_iff_lt_add.2 (norm_add_lt_of_not_sameRay fun H' => h <| H'.add_left SameRay.rfl)

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