oangle_center_eq_two_zsmul_oangle

English

For a circle, the angle at the center between p1 and p3 equals twice the angle at p2 in the triangle p1-p2-p3 on the circle.

Русский

Для окружности угол в центре между p1 и p3 равен удвоенному углу в точке p2 треугольника p1-p2-p3 на окружности.

LaTeX

$$$\\angle(p_1, s.center, p_3) = 2\\,\\angle(p_1, p_2, p_3)$$$

Lean4

/-- Angle at center of a circle equals twice angle at circumference, oriented angle version. -/
theorem oangle_center_eq_two_zsmul_oangle {s : Sphere P} {p₁ p₂ p₃ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s)
    (hp₂p₁ : p₂ ≠ p₁) (hp₂p₃ : p₂ ≠ p₃) : ∡ p₁ s.center p₃ = (2 : ℤ) • ∡ p₁ p₂ p₃ :=
  by
  rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃
  rw [oangle, oangle, «o».oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real _ _ hp₂ hp₁ hp₃] <;> simp [hp₂p₁, hp₂p₃]

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