English
Let V be a real vector space and consider a 2-dimensional subspace. For centers c1 ≠ c2 and two points p1 ≠ p2 lying in the same plane with equal distances to c1 and to c2 (r1 and r2 respectively), any other point p in the plane equidistant from c1 and c2 with the same radii must coincide with p1 or p2.
Русский
Пусть V — вещественное пространство, а направление пространства имеет размерность 2. Пусть c1 ≠ c2 и p1 ≠ p2 лежат в одной плоскости; если dist(p1,c1)=dist(p2,c1)=r1 и dist(p1,c2)=dist(p2,c2)=r2, и p ∈ плоскость удовлетворяет dist(p,c1)=r1, dist(p,c2)=r2, тогда p равно p1 или p2.
LaTeX
$$$\\forall V,P\\; [\\dim(V)=2] \\Rightarrow\\forall c_1,c_2,p_1,p_2,p\\in P,\\ c_1 \\neq c_2,\\ p_1 \\neq p_2,\\ p_i, p \\in V \\ (i=1,2),\\ dist(p_1,c_1)=dist(p_2,c_1)=r_1,\\ dist(p_1,c_2)=dist(p_2,c_2)=r_2,\\ dist(p,c_1)=r_1,\\ dist(p,c_2)=r_2 \\Rightarrow p = p_1 \\lor p = p_2.$$$
Lean4
/-- Distances `r₁` `r₂` of `p` from two different points `c₁` `c₂` determine at
most two points `p₁` `p₂` in two-dimensional space (two circles intersect in at
most two points). -/
theorem eq_of_dist_eq_of_dist_eq_of_finrank_eq_two [FiniteDimensional ℝ V] (hd : finrank ℝ V = 2) {c₁ c₂ p₁ p₂ p : P}
{r₁ r₂ : ℝ} (hc : c₁ ≠ c₂) (hp : p₁ ≠ p₂) (hp₁c₁ : dist p₁ c₁ = r₁) (hp₂c₁ : dist p₂ c₁ = r₁)
(hpc₁ : dist p c₁ = r₁) (hp₁c₂ : dist p₁ c₂ = r₂) (hp₂c₂ : dist p₂ c₂ = r₂) (hpc₂ : dist p c₂ = r₂) :
p = p₁ ∨ p = p₂ :=
haveI hd' : finrank ℝ (⊤ : AffineSubspace ℝ P).direction = 2 :=
by
rw [direction_top, finrank_top]
exact hd
eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two hd' (mem_top ℝ V _) (mem_top ℝ V _) (mem_top ℝ V _) (mem_top ℝ V _)
(mem_top ℝ V _) hc hp hp₁c₁ hp₂c₁ hpc₁ hp₁c₂ hp₂c₂ hpc₂
