English
Let S be a two-dimensional affine subspace of a Euclidean space. Take two distinct centers c1, c2 in S and two distinct points p1, p2 in S. Suppose the distances dist(p1, c1) = dist(p2, c1) = r1 and dist(p1, c2) = dist(p2, c2) = r2, and further a point p ∈ S satisfies dist(p, c1) = r1 and dist(p, c2) = r2. Then p must be either p1 or p2.
Русский
Пусть S — двумерное аффинное подпроstranstvo Евклидового пространства. Возьмем два различных центра c1, c2 в S и две точки p1, p2 в S. Пусть dist(p1, c1) = dist(p2, c1) = r1 и dist(p1, c2) = dist(p2, c2) = r2, и пусть точка p ∈ S удовлетворяет dist(p, c1) = r1 и dist(p, c2) = r2. Тогда p равно либо p1, либо p2.
LaTeX
$$$\\forall s\\;[\\text{FinRank}(\\mathrm{dir}(s)) = 2]\\;\\Rightarrow\\forall c_1,c_2,p_1,p_2,p\\in P\\;\\Big( c_1 \\neq c_2 \\land p_1 \\neq p_2 \\land p_1,p_2,p,c_1,c_2 \\in s \\land \\ dist(p_1,c_1)=\\ dist(p_2,c_1)=r_1 \\land \\ dist(p_1,c_2)=\\ dist(p_2,c_2)=r_2 \\land \\ dist(p,c_1)=r_1 \\land \\ dist(p,c_2)=r_2 \\Big) \\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 a two-dimensional subspace containing those points
(two circles intersect in at most two points). -/
theorem eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two {s : AffineSubspace ℝ P} [FiniteDimensional ℝ s.direction]
(hd : finrank ℝ s.direction = 2) {c₁ c₂ p₁ p₂ p : P} (hc₁s : c₁ ∈ s) (hc₂s : c₂ ∈ s) (hp₁s : p₁ ∈ s) (hp₂s : p₂ ∈ s)
(hps : p ∈ s) {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₂ :=
by
have ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0 :=
inner_vsub_vsub_of_dist_eq_of_dist_eq (hp₁c₁.trans hp₂c₁.symm) (hp₁c₂.trans hp₂c₂.symm)
have hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0 :=
inner_vsub_vsub_of_dist_eq_of_dist_eq (hp₁c₁.trans hpc₁.symm) (hp₁c₂.trans hpc₂.symm)
let b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
have hb : LinearIndependent ℝ b :=
by
refine linearIndependent_of_ne_zero_of_inner_eq_zero ?_ ?_
· intro i
fin_cases i <;> simp [b, hc.symm, hp.symm]
· intro i j hij
fin_cases i <;> fin_cases j <;> try exact False.elim (hij rfl)
· exact ho
· rw [real_inner_comm]
exact ho
have hbs : Submodule.span ℝ (Set.range b) = s.direction :=
by
refine Submodule.eq_of_le_of_finrank_eq ?_ ?_
· rw [Submodule.span_le, Set.range_subset_iff]
intro i
fin_cases i
· exact vsub_mem_direction hc₂s hc₁s
· exact vsub_mem_direction hp₂s hp₁s
· rw [finrank_span_eq_card hb, Fintype.card_fin, hd]
have hv : ∀ v ∈ s.direction, ∃ t₁ t₂ : ℝ, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁) :=
by
intro v hv
have hr : Set.range b = {c₂ -ᵥ c₁, p₂ -ᵥ p₁} :=
by
have hu : (Finset.univ : Finset (Fin 2)) = {0, 1} := by decide
classical
rw [← Fintype.coe_image_univ, hu]
simp [b]
rw [← hbs, hr, Submodule.mem_span_insert] at hv
rcases hv with ⟨t₁, v', hv', hv⟩
rw [Submodule.mem_span_singleton] at hv'
rcases hv' with ⟨t₂, rfl⟩
exact ⟨t₁, t₂, hv⟩
rcases hv (p -ᵥ p₁) (vsub_mem_direction hps hp₁s) with ⟨t₁, t₂, hpt⟩
simp only [hpt, inner_add_right, inner_smul_right, ho, mul_zero, add_zero, mul_eq_zero, inner_self_eq_zero,
vsub_eq_zero_iff_eq, hc.symm, or_false] at hop
rw [hop, zero_smul, zero_add, ← eq_vadd_iff_vsub_eq] at hpt
subst hpt
have hp' : (p₂ -ᵥ p₁ : V) ≠ 0 := by simp [hp.symm]
have hp₂ : dist ((1 : ℝ) • (p₂ -ᵥ p₁) +ᵥ p₁) c₁ = r₁ := by simp [hp₂c₁]
rw [← hp₁c₁, dist_smul_vadd_eq_dist _ _ hp'] at hpc₁ hp₂
simp only [one_ne_zero, false_or] at hp₂
rw [hp₂.symm] at hpc₁
rcases hpc₁ with hpc₁ | hpc₁ <;> simp [hpc₁]
