sameRay_iff_norm_smul_eq — Mathlib

English

For nonzero x,y, x and y are on the same ray if and only if the unit vectors ‖x‖⁻¹·x and ‖y‖⁻¹·y are equal.

Русский

Для ненулевых x,y лучи совпадают тогда и только тогда, когда единичные векторы ‖x‖⁻¹·x и ‖y‖⁻¹·y совпадают.

LaTeX

$$$$ \forall x,y \neq 0,\; \text{SameRay}(\mathbb{R},x,y) \iff \|x\|^{-1}x = \|y\|^{-1}y. $$$$

Lean4

theorem sameRay_iff_norm_smul_eq : SameRay ℝ x y ↔ ‖x‖ • y = ‖y‖ • x :=
  ⟨SameRay.norm_smul_eq, fun h =>
    or_iff_not_imp_left.2 fun hx =>
      or_iff_not_imp_left.2 fun hy => ⟨‖y‖, ‖x‖, norm_pos_iff.2 hy, norm_pos_iff.2 hx, h.symm⟩⟩

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