English
Let s be a sphere in a Euclidean space and a, b, p be points with a and b on s, and p lying on the line through a and b. If p also lies on s, then the product of the distances from p to a and from p to b is zero; i.e. either p = a or p = b.
Русский
Пусть s — сфера в евклидовом пространстве, точки a, b лежат на s, p лежит на прямой через a и b и также принадлежит s. Тогда произведение расстояний dist(p,a)·dist(p,b) = 0; следовательно, либо p = a, либо p = b.
LaTeX
$$$\forall s\colon \text{Sphere}(P),\; p,a,b\in P:\; p\in \mathrm{line}(a,b) \land a\in s \land b\in s \land p\in s \Rightarrow \operatorname{dist}(p,a)\operatorname{dist}(p,b)=0$$$
Lean4
/-- For a point on the sphere, the product of distances to two other intersection
points on a line through the point is zero. -/
theorem mul_dist_eq_zero_of_mem_sphere {s : Sphere P} {p a b : P} (hp : p ∈ line[ℝ, a, b]) (ha : a ∈ s) (hb : b ∈ s)
(hp_on : p ∈ s) : dist p a * dist p b = 0 :=
by
have hq : dist a s.center = dist b s.center := by rw [mem_sphere.mp ha, mem_sphere.mp hb]
rw [dist_comm p a, dist_comm p b, mul_dist_eq_abs_sub_sq_dist hp hq, mem_sphere.mp hb, mem_sphere.mp hp_on, sub_self,
abs_zero]
