oangle_add_oangle_rev — Mathlib

English

The sum of two adjacent oriented angles equals the angle formed by the outer rays: ∡ p1 p p2 + ∡ p2 p p3 = ∡ p1 p p3, provided p, p1, p2, p3 are distinct appropriately.

Русский

Сумма двух смежных ориентированных углов равна углу между внешними лучами: ∡ p1 p p2 + ∡ p2 p p3 = ∡ p1 p p3, если точки различны соответствующим образом.

LaTeX

$$$ \forall p,p_1,p_2,p_3 : P,\ (p_1 \neq p) \land (p_2 \neq p) \land (p_3 \neq p) \rightarrow\ Eq (\angle p_1 p p_2 + \angle p_2 p p_3) (\angle p_1 p p_3)$$$

Lean4

/-- Adding an angle to that with the order of the points reversed results in 0. -/
@[simp]
theorem oangle_add_oangle_rev (p₁ p₂ p₃ : P) : ∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₁ = 0 :=
  o.oangle_add_oangle_rev _ _

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