angle_eq_pi_div_two_iff_mem_sphere_ofDiameter

English

The same as Thales’ Theorem framed with a diameter condition via the sphere of diameter p1-p3.

Русский

То же самое, что и теорема Талеса, сформулированное через диаметр p1-p3 в рамках сферы.

LaTeX

$$$\\angle p_1 p_2 p_3 = \\pi/2 \\iff p_2 \\in \\mathrm{Sphere}.ofDiameter(p_1,p_3)$$$

Lean4

/-- **Thales' theorem**: For three distinct points, the angle at the second point
is a right angle if and only if the second point lies on the sphere having the first and third
points as diameter endpoints. -/
theorem angle_eq_pi_div_two_iff_mem_sphere_ofDiameter {p₁ p₂ p₃ : P} :
    ∠ p₁ p₂ p₃ = π / 2 ↔ p₂ ∈ Sphere.ofDiameter p₁ p₃ :=
  angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter (Sphere.isDiameter_ofDiameter p₁ p₃)

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