sameRay_iff_norm_sub — Mathlib

English

Two vectors are in the same ray if and only if ∥x−y∥ = |∥x∥ − ∥y∥|.

Русский

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

LaTeX

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

Lean4

theorem sameRay_iff_norm_sub : SameRay ℝ x y ↔ ‖x - y‖ = |‖x‖ - ‖y‖| :=
  ⟨SameRay.norm_sub, fun h => Classical.not_not.1 fun h' => (abs_lt_norm_sub_of_not_sameRay h').ne' h⟩

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