sameRay_iff_inv_norm_smul_eq_of_ne

English

When both x and y are nonzero, SameRay x y is equivalent to equality of the scaled unit vectors, i.e., ‖x‖⁻¹·x = ‖y‖⁻¹·y.

Русский

При x,y ≠ 0 равенство луча эквивалентно равенству нормированных векторов: ‖x‖⁻¹·x = ‖y‖⁻¹·y.

LaTeX

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

Lean4

/-- Two nonzero vectors `x y` in a real normed space are on the same ray if and only if the unit
vectors `‖x‖⁻¹ • x` and `‖y‖⁻¹ • y` are equal. -/
theorem sameRay_iff_inv_norm_smul_eq_of_ne (hx : x ≠ 0) (hy : y ≠ 0) : SameRay ℝ x y ↔ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y := by
  rw [inv_smul_eq_iff₀, smul_comm, eq_comm, inv_smul_eq_iff₀, sameRay_iff_norm_smul_eq] <;> rwa [norm_ne_zero_iff]

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