oangle_eq_iff_eq_norm_div_norm_smul_rotation_or_eq_zero

English

The angle between x and y is θ if and only if either both are nonzero with a rotation representation, or θ = 0 and at least one of x,y is zero.

Русский

Угол между x и y равен θ тогда и только тогда либо оба ненулевые и равенство через вращение, либо θ = 0 и хотя бы один из x,y равен нулю.

LaTeX

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

Lean4

/-- The angle between two vectors is `θ` if and only if they are nonzero and the second vector
is the first rotated by `θ` and scaled by the ratio of the norms, or `θ` and at least one of the
vectors are zero. -/
theorem oangle_eq_iff_eq_norm_div_norm_smul_rotation_or_eq_zero {x y : V} (θ : Real.Angle) :
    o.oangle x y = θ ↔ x ≠ 0 ∧ y ≠ 0 ∧ y = (‖y‖ / ‖x‖) • o.rotation θ x ∨ θ = 0 ∧ (x = 0 ∨ y = 0) :=
  by
  by_cases hx : x = 0
  · simp [hx, eq_comm]
  · by_cases hy : y = 0
    · simp [hy, eq_comm]
    · rw [o.oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero hx hy]
      simp [hx, hy]

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