English
On a sphere, for a tangent at t from p and secant through p meeting a and b on the sphere, the tangent length squared equals the product of the secant lengths: dist(p,t)^2 = dist(p,a) dist(p,b).
Русский
На сфере касательная длина в точке t от p в квадрате равна произведению длин секант через p до точек a и b на сфере: dist(p,t)^2 = dist(p,a) dist(p,b).
LaTeX
$$$\\operatorname{dist}(p,t)^2 = \\operatorname{dist}(p,a) \\cdot \\operatorname{dist}(p,b)$$$
Lean4
/-- **Tangent-Secant Theorem**. The square of the tangent length equals
the product of secant segment lengths. -/
theorem dist_sq_eq_mul_dist_of_tangent_and_secant {a b t p : P} {s : Sphere P} (ha : a ∈ s) (hb : b ∈ s)
(hp : p ∈ line[ℝ, a, b]) (h_tangent : s.IsTangentAt t (line[ℝ, p, t])) : dist p t ^ 2 = dist p a * dist p b :=
by
have hr := radius_nonneg_of_mem ha
have radius_le_dist := h_tangent.isTangent.radius_le_dist_center (left_mem_affineSpan_pair ℝ p t)
rw [mul_dist_eq_power_of_radius_le_dist_center hr hp ha hb radius_le_dist, Sphere.power,
h_tangent.dist_sq_eq_of_mem (left_mem_affineSpan_pair ℝ p t)]
ring
