oangle_eq_pi_sub_two_zsmul_oangle_center_left

English

For two points on a circle, the base angle at the center is acute in absolute value.

Русский

Для двух точек на окружности основанный угол в центре острый по модулю.

LaTeX

$$|(oangle(s.center, p2, p1)).toReal| < \\pi/2$$

Lean4

/-- The angle at the apex of an isosceles triangle is `π` minus twice a base angle, oriented
angle-at-point form where the apex is given as the center of a circle. -/
theorem oangle_eq_pi_sub_two_zsmul_oangle_center_left {s : Sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s)
    (h : p₁ ≠ p₂) : ∡ p₁ s.center p₂ = π - (2 : ℤ) • ∡ s.center p₂ p₁ := by
  rw [oangle_eq_pi_sub_two_zsmul_oangle_of_dist_eq h.symm (dist_center_eq_dist_center_of_mem_sphere' hp₂ hp₁)]

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