oangle_eq_pi_iff_oangle_rev_eq_pi

English

The oriented angle between x and y equals π if and only if the angle between y and x equals π.

Русский

Угол между x и y равен π тогда и только тогда, когда угол между y и x равен π.

LaTeX

$$$o.oangle x y = \pi \iff o.oangle y x = \pi$$$

Lean4

/-- The oriented angle between two vectors is `π` if and only if the angle with the vectors
swapped is `π`. -/
theorem oangle_eq_pi_iff_oangle_rev_eq_pi {x y : V} : o.oangle x y = π ↔ o.oangle y x = π := by
  rw [oangle_rev, neg_eq_iff_eq_neg, Real.Angle.neg_coe_pi]

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