English
For any p1, p2 on two spheres s1, s2 with centers in a 2D subspace, if p1 and p2 are distinct, then the intersection of the spheres has at most two points, namely p1 and p2.
Русский
Для любых точек p1, p2 на сферах s1, s2 с центрами в двумерном подпространстве, если p1 ≠ p2, пересечение сфер содержит не более двух точек: p1 и p2.
LaTeX
$$$\text{IsTwoPoints}(s_1,s_2, p_1,p_2)\Rightarrow p\in s_1\cap s_2\Rightarrow p=p_1\lor p=p_2$$$
Lean4
/-- Two spheres intersect in at most two points in a two-dimensional subspace containing their
centers; this is a version of `eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two` for bundled
spheres. -/
theorem eq_of_mem_sphere_of_mem_sphere_of_mem_of_finrank_eq_two {s : AffineSubspace ℝ P}
[FiniteDimensional ℝ s.direction] (hd : finrank ℝ s.direction = 2) {s₁ s₂ : Sphere P} {p₁ p₂ p : P}
(hs₁ : s₁.center ∈ s) (hs₂ : s₂.center ∈ s) (hp₁s : p₁ ∈ s) (hp₂s : p₂ ∈ s) (hps : p ∈ s) (hs : s₁ ≠ s₂)
(hp : p₁ ≠ p₂) (hp₁s₁ : p₁ ∈ s₁) (hp₂s₁ : p₂ ∈ s₁) (hps₁ : p ∈ s₁) (hp₁s₂ : p₁ ∈ s₂) (hp₂s₂ : p₂ ∈ s₂)
(hps₂ : p ∈ s₂) : p = p₁ ∨ p = p₂ :=
eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two hd hs₁ hs₂ hp₁s hp₂s hps
((Sphere.center_ne_iff_ne_of_mem hps₁ hps₂).2 hs) hp hp₁s₁ hp₂s₁ hps₁ hp₁s₂ hp₂s₂ hps₂
