oangle_eq_zero_iff_angle_eq_zero — Mathlib

English

For nonzero x,y, the oriented angle is zero if and only if the unoriented angle is zero.

Русский

Для ненулевых векторов x,y ориентированный угол равен нулю тогда и только тогда, когда неориентированный угол равен нулю.

LaTeX

$$$ x \neq 0 \land y \neq 0 \Rightarrow o.oangle x y = 0 \iff InnerProductGeometry.angle x y = 0 $$$

Lean4

/-- The oriented angle between two nonzero vectors is zero if and only if the unoriented angle
is zero. -/
theorem oangle_eq_zero_iff_angle_eq_zero {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
    o.oangle x y = 0 ↔ InnerProductGeometry.angle x y = 0 :=
  by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · simpa [o.angle_eq_abs_oangle_toReal hx hy]
  · have ha := o.oangle_eq_angle_or_eq_neg_angle hx hy
    rw [h] at ha
    simpa using ha

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