oangle_add_oangle_rev — Mathlib

English

The sum of the oriented angles in both orders is zero: o.oangle x y + o.oangle y x = 0.

Русский

Сумма ориентированных углов в двух направлениях равна нулю: o.oangle x y + o.oangle y x = 0.

LaTeX

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

Lean4

/-- Adding the angles between two vectors in each order results in 0. -/
@[simp]
theorem oangle_add_oangle_rev (x y : V) : o.oangle x y + o.oangle y x = 0 := by simp [o.oangle_rev y x]

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