English
In a configuration where a, b lie on a sphere s and the line through a and b passes through p, if t is a point where the line through p and t is tangent to s, then the tangent length squared equals the product of the two secant lengths: dist(p,t)^2 = dist(p,a) dist(p,b).
Русский
В конфигурации, где a и b лежат на сфере s, прямая через a и b проходит через p, и t — точка касания сферы касательной через p и t, тогда квадраты касательной длины равны произведению длин секущих: dist(p,t)^2 = dist(p,a) dist(p,b).
LaTeX
$$$\forall a,b,t,p:\; a,b\in s \land p\in \mathrm{line}(a,b) \land s.IsTangentAt t (\mathrm{line}(p,t))\Rightarrow \operatorname{dist}(p,t)^2=\operatorname{dist}(p,a)\operatorname{dist}(p,b)$$$
Lean4
/-- For a point inside or on the sphere, the product of distances to two intersection
points on a line through the point equals the negative of the power of the point. -/
theorem mul_dist_eq_neg_power_of_dist_center_le_radius {s : Sphere P} {p a b : P} (hr : 0 ≤ s.radius)
(hp : p ∈ line[ℝ, a, b]) (ha : a ∈ s) (hb : b ∈ s) (hle : dist p s.center ≤ s.radius) :
dist p a * dist p b = -s.power p := by
rw [mul_dist_eq_abs_power hp ha hb, abs_of_nonpos <| (power_nonpos_iff_dist_center_le_radius hr).mpr hle]
