oangle_sub_right — Mathlib

English

If x,y,z are nonzero, then o.oangle(-x) y + o.oangle(-y) z + o.oangle(-z) x = π.

Русский

Если x,y,z не нулевые, то o.oangle(-x) y + o.oangle(-y) z + o.oangle(-z) x = π.

LaTeX

$$o.oangle(-x) y + o.oangle(-y) z + o.oangle(-z) x = \pi$$

Lean4

/-- Given three nonzero vectors, the angle between the first and the third minus the angle
between the second and the third equals the angle between the first and the second. -/
@[simp]
theorem oangle_sub_right {x y z : V} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) :
    o.oangle x z - o.oangle y z = o.oangle x y := by rw [sub_eq_iff_eq_add, o.oangle_add hx hy hz]

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