English
If s1 and s2 are internally tangent, then dist(s1.center, s2.center) equals the difference of radii.
Русский
Если сферы s1 и s2 внутренне касаются, расстояние между центрами равно разности радиусов.
LaTeX
$$$\operatorname{dist}(s_1.center, s_2.center) = s_2.radius - s_1.radius$$$
Lean4
theorem isExtTangent_iff_dist_center {s₁ s₂ : Sphere P} :
s₁.IsExtTangent s₂ ↔ dist s₁.center s₂.center = s₁.radius + s₂.radius ∧ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius :=
by
refine ⟨fun h ↦ ⟨h.dist_center, ?_⟩, ?_⟩
· rcases h with ⟨p, h₁, h₂, h⟩
exact ⟨radius_nonneg_of_mem h₁, radius_nonneg_of_mem h₂⟩
· rintro ⟨h, h₁, h₂⟩
refine ⟨AffineMap.lineMap s₁.center s₂.center (s₁.radius / (s₁.radius + s₂.radius)), ?_⟩
by_cases h0 : s₁.radius + s₂.radius = 0
· simp only [h0, div_zero, AffineMap.lineMap_apply_zero, isExtTangentAt_center_iff, mem_sphere]
exact ⟨by linarith, by linarith⟩
· refine ⟨?_, ?_, ?_⟩
· simp only [mem_sphere, dist_lineMap_left, norm_div, Real.norm_eq_abs, h, abs_of_nonneg h₁,
abs_of_nonneg (add_nonneg h₁ h₂)]
field_simp
· simp only [mem_sphere, dist_lineMap_right, Real.norm_eq_abs, h]
rw [one_sub_div h0, add_sub_cancel_left, abs_div, abs_of_nonneg h₂, abs_of_nonneg (add_nonneg h₁ h₂)]
field_simp
· simp only [wbtw_lineMap_iff]
refine .inr ⟨?_, ?_⟩
· positivity
· rw [div_le_one (by positivity)]
linarith
