English
In a two-dimensional subspace, the intersection of two spheres is at most two points. If p1, p2 lie on spheres s1 and s2 respectively and a point p lies in their common plane, then p equals p1 or p2 under the given non-degeneracy assumptions.
Русский
Во двумерном подпространстве пересечение двух сфер имеет не более двух точек; если p1,p2 лежат на сферах s1,s2 соответственно и точка p лежит в их общей плоскости, то p равно p1 или p2 при заданных допущениях.
LaTeX
$$$\text{eq_of_mem_sphere_of_mem_sphere_of_mem_of_finrank_eq_two}\left( hd, hs, hp_1s, hp_2s, hps, hs, hp, hp_1s_1, hp_2s_1, hps_1, hp_1s_2, hp_2s_2, hps_2 \right) \Rightarrow p = p_1 \lor p = p_2$$$
Lean4
/-- Suppose that `p₁` and `p₂` lie in spheres `s₁` and `s₂`. Then the vector between the centers
of those spheres is orthogonal to that between `p₁` and `p₂`; this is a version of
`inner_vsub_vsub_of_dist_eq_of_dist_eq` for bundled spheres. (In two dimensions, this says that
the diagonals of a kite are orthogonal.) -/
theorem inner_vsub_vsub_of_mem_sphere_of_mem_sphere {p₁ p₂ : P} {s₁ s₂ : Sphere P} (hp₁s₁ : p₁ ∈ s₁) (hp₂s₁ : p₂ ∈ s₁)
(hp₁s₂ : p₁ ∈ s₂) (hp₂s₂ : p₂ ∈ s₂) : ⟪s₂.center -ᵥ s₁.center, p₂ -ᵥ p₁⟫ = 0 :=
inner_vsub_vsub_of_dist_eq_of_dist_eq (dist_center_eq_dist_center_of_mem_sphere hp₁s₁ hp₂s₁)
(dist_center_eq_dist_center_of_mem_sphere hp₁s₂ hp₂s₂)
