oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero

English

If x and y are nonzero, the angle between them is θ if and only if there exists a positive scalar r with y = r · o.rotation θ x.

Русский

Если x и y ненулевые, угол между ними равен θ тогда и только тогда существует положительное число r, такое что y = r · o.rotation θ x.

LaTeX

$$x ≠ 0 ∧ y ≠ 0 → o.oangle x y = θ ↔ ∃ r>0, y = r • o.rotation θ x$$

Lean4

/-- The angle between two nonzero vectors is `θ` if and only if the second vector is the first
rotated by `θ` and scaled by a positive real. -/
theorem oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) (θ : Real.Angle) :
    o.oangle x y = θ ↔ ∃ r : ℝ, 0 < r ∧ y = r • o.rotation θ x :=
  by
  constructor
  · intro h
    rw [o.oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero hx hy] at h
    exact ⟨‖y‖ / ‖x‖, div_pos (norm_pos_iff.2 hy) (norm_pos_iff.2 hx), h⟩
  · rintro ⟨r, hr, rfl⟩
    rw [o.oangle_smul_right_of_pos _ _ hr, o.oangle_rotation_self_right hx]

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