angle_add_angle_sub_add_angle_sub_eq_pi

English

The sum of the three interior angles of a triangle (possibly degenerate) is π.

Русский

Сумма трех внутренних углов треугольника (возможно вырожденного) равна π.

LaTeX

$$$\angle p_1 p_2 p_3 + \angle p_2 p_3 p_1 + \angle p_3 p_1 p_2 = \pi$$$

Lean4

/-- The sum of the angles of a possibly degenerate triangle (where one of the
two given sides is nonzero), vector angle form. -/
theorem angle_add_angle_sub_add_angle_sub_eq_pi (x : V) {y : V} (hy : y ≠ 0) :
    angle x y + angle x (x - y) + angle y (y - x) = π :=
  by
  have h := angle_eq_angle_add_add_angle_add (x - y) hy
  rw [sub_add_cancel] at h
  rw [← neg_sub x y, angle_neg_right]
  simp only [angle_comm] at h ⊢
  linear_combination -h

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