oangle_add_swap — Mathlib

English

The sum of the angle ∡ p1 p p2 and the reversed angle ∡ p3 p p1 equals ∡ p3 p p2.

Русский

Сумма угла ∡ p1 p p2 и перевернутого угла ∡ p3 p p1 равна ∡ p3 p p2.

LaTeX

$$$ \forall p,p_1,p_2,p_3 : P,\ (\angle p_1 p p_2) + (\angle p_3 p p_1) = (\angle p_3 p p_2)$$$

Lean4

/-- Given three points not equal to `p`, the angle between the second and the third at `p` plus
the angle between the first and the second equals the angle between the first and the third. -/
@[simp]
theorem oangle_add_swap {p p₁ p₂ p₃ : P} (hp₁ : p₁ ≠ p) (hp₂ : p₂ ≠ p) (hp₃ : p₃ ≠ p) :
    ∡ p₂ p p₃ + ∡ p₁ p p₂ = ∡ p₁ p p₃ :=
  o.oangle_add_swap (vsub_ne_zero.2 hp₁) (vsub_ne_zero.2 hp₂) (vsub_ne_zero.2 hp₃)

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