English
The sum of oriented angles around a triangle equals π, even with degeneracy.
Русский
Сумма ориентированных углов треугольника равна π, даже при вырожденности.
LaTeX
$$$\angle x y p + \angle y p x + \angle p x y = \pi$$$
Lean4
/-- The **sum of the angles of a triangle** (possibly degenerate, where two
given vertices are distinct), angle-at-point. -/
theorem angle_add_angle_add_angle_eq_pi {p₁ p₂ : P} (p₃ : P) (h : p₂ ≠ p₁) : ∠ p₁ p₂ p₃ + ∠ p₂ p₃ p₁ + ∠ p₃ p₁ p₂ = π :=
by
rw [add_assoc, add_comm, add_comm (∠ p₂ p₃ p₁), angle_comm p₂ p₃ p₁]
unfold angle
rw [← angle_neg_neg (p₁ -ᵥ p₃), ← angle_neg_neg (p₁ -ᵥ p₂), neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev,
neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev, ← vsub_sub_vsub_cancel_right p₃ p₂ p₁, ←
vsub_sub_vsub_cancel_right p₂ p₃ p₁]
exact angle_add_angle_sub_add_angle_sub_eq_pi _ fun he => h (vsub_eq_zero_iff_eq.1 he)
