not_sameRay_iff_abs_lt_norm_sub — Mathlib

English

Two vectors are not on the same ray if and only if |∥x∥ − ∥y∥| < ∥x−y∥.

Русский

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

LaTeX

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

Lean4

theorem not_sameRay_iff_abs_lt_norm_sub : ¬SameRay ℝ x y ↔ |‖x‖ - ‖y‖| < ‖x - y‖ :=
  sameRay_iff_norm_sub.not.trans <| ne_comm.trans (abs_norm_sub_norm_le _ _).lt_iff_ne.symm

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