oangle_eq_zero_iff_oangle_rev_eq_zero

English

The oriented angle between x and y is zero if and only if the angle between y and x is zero.

Русский

Ориентированный угол между x и y равен нулю тогда и только тогда, когда угол между y и x равен нулю.

LaTeX

$$$o.oangle x y = 0 \;\Leftrightarrow\; o.oangle y x = 0$$$

Lean4

/-- The oriented angle between two vectors is zero if and only if the angle with the vectors
swapped is zero. -/
theorem oangle_eq_zero_iff_oangle_rev_eq_zero {x y : V} : o.oangle x y = 0 ↔ o.oangle y x = 0 := by
  rw [oangle_rev, neg_eq_zero]

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