oangle_add_swap — Mathlib

English

The sum of the angles o.oangle y z + o.oangle x y equals o.oangle x z (cyclic permutation).

Русский

Сумма углов o.oangle y z + o.oangle x y равна o.oangle x z (по циклу).

LaTeX

$$$o.oangle y z + o.oangle x y = o.oangle x z$$$

Lean4

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

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