dist_div_sin_oangle_eq_two_mul_radius

English

If four points lie on a circle, the two doubled center-based angles are equal.

Русский

Если четыре точки лежат на окружности, дважды центрированные углы равны.

LaTeX

$$$2\\ oangle p_1 p_2 p_4 = 2\\ oangle p_1 p_3 p_4$$$

Lean4

/-- Given three points on a circle, twice the radius of that circle may be expressed explicitly as
the distance between two of those points divided by the absolute value of the sine of the angle
at the third point (a version of the law of sines or sine rule). -/
theorem dist_div_sin_oangle_eq_two_mul_radius {s : Sphere P} {p₁ p₂ p₃ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s)
    (hp₁p₂ : p₁ ≠ p₂) (hp₁p₃ : p₁ ≠ p₃) (hp₂p₃ : p₂ ≠ p₃) : dist p₁ p₃ / |Real.Angle.sin (∡ p₁ p₂ p₃)| = 2 * s.radius :=
  by rw [← dist_div_sin_oangle_div_two_eq_radius hp₁ hp₂ hp₃ hp₁p₂ hp₁p₃ hp₂p₃, mul_div_cancel₀ _ (two_ne_zero' ℝ)]

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