English
If the center subspace has dimension 2, the intersection of two spheres is at most two points; more precisely, if p1,p2 are centers and p is a point in both spheres with p1 ≠ p2, then p ∈ {p1,p2}.
Русский
Если подпространство центров имеет размерность 2, пересечение двух сфер состоит не более чем из двух точек; если p1,p2 — центры сфер, и p лежит на обеих сферах, при p1 ≠ p2, тогда p принадлежит {p1,p2}.
LaTeX
$$$\text{p} \in s_1\cap s_2\Rightarrow p=p_1\lor p=p_2$ under finrank 2 assumptions$$
Lean4
/-- Two spheres intersect in at most two points in two-dimensional space; this is a version of
`eq_of_dist_eq_of_dist_eq_of_finrank_eq_two` for bundled spheres. -/
theorem eq_of_mem_sphere_of_mem_sphere_of_finrank_eq_two [FiniteDimensional ℝ V] (hd : finrank ℝ V = 2)
{s₁ s₂ : Sphere P} {p₁ p₂ p : P} (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_finrank_eq_two hd ((Sphere.center_ne_iff_ne_of_mem hps₁ hps₂).2 hs) hp hp₁s₁ hp₂s₁ hps₁
hp₁s₂ hp₂s₂ hps₂
