English
For any three distinct points p1, p2, p3 on a circle, the angle at p2 formed by p1-p2-p3 is a right angle if and only if p2 lies on the circle with diameter p1-p3.
Русский
Для любых трёх различных точек p1, p2, p3 на окружности угол p1-p2-p3 равен π/2 тогда и только тогда, когда p2 лежит на сфере диаметра p1-p3.
LaTeX
$$$\\angle p_1 p_2 p_3 = \\frac{\\pi}{2} \\iff p_2 \\in \\mathrm{Sphere}.ofDiameter(p_1, p_3)$$$
Lean4
/-- **Thales' theorem**: The angle inscribed in a semicircle is a right angle. -/
theorem angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter {p₁ p₂ p₃ : P} {s : Sphere P} (hd : s.IsDiameter p₁ p₃) :
∠ p₁ p₂ p₃ = π / 2 ↔ p₂ ∈ s :=
by
rw [mem_sphere', EuclideanGeometry.angle, ← InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two]
let o := s.center
have h_center : o = midpoint ℝ p₁ p₃ := hd.midpoint_eq_center.symm
rw [← vsub_add_vsub_cancel p₁ o p₂, ← vsub_add_vsub_cancel p₃ o p₂, inner_add_left, inner_add_right, inner_add_right]
have h_opp : p₁ -ᵥ o = -(p₃ -ᵥ o) := by
rw [h_center, left_vsub_midpoint, right_vsub_midpoint, ← smul_neg, neg_vsub_eq_vsub_rev]
rw [h_opp, inner_neg_left, inner_neg_left, real_inner_comm (p₃ -ᵥ o) (o -ᵥ p₂)]
ring_nf
rw [neg_add_eq_zero, real_inner_self_eq_norm_sq, ← dist_eq_norm_vsub, real_inner_self_eq_norm_sq, ← dist_eq_norm_vsub,
sq_eq_sq₀ dist_nonneg dist_nonneg, mem_sphere.mp hd.right_mem]
exact eq_comm
