oangle_add_cyc3 — Mathlib

English

For nonzero x,y,z, the sum o.oangle x (-y) + o.oangle y (-z) + o.oangle z (-x) equals π.

Русский

Для ненулевых 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) = π$$

Lean4

/-- Given three nonzero vectors, adding the angles between them in cyclic order results in 0. -/
theorem oangle_add_cyc3 {x y z : V} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) :
    o.oangle x y + o.oangle y z + o.oangle z x = 0 := by simp [hx, hy, hz]

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