English
For nontrivial spaces, s1 IsIntTangent s2 if and only if dist centers equals s2.radius − s1.radius and radii are nonnegative.
Русский
Для ненулевых пространств s1 IsIntTangent s2 тогда и только тогда, когда dist центров равно s2.radius − s1.radius, и радиусы неотрицательны.
LaTeX
$$$s_1\IsIntTangent s_2 \iff \operatorname{dist}(s_1.center, s_2.center) = s_2.radius - s_1.radius \land 0 \le s_1.radius \land 0 \le s_2.radius$$$
Lean4
theorem isIntTangent_iff_dist_center [Nontrivial V] {s₁ s₂ : Sphere P} :
s₁.IsIntTangent 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₂⟩
by_cases h0 : s₁.center = s₂.center
· rw [h0, dist_self, eq_comm, sub_eq_zero, eq_comm] at h
have hs : s₁ = s₂ := by ext <;> assumption
simp [hs, h₂]
· rw [dist_comm] at h
have ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius :=
by
refine abs_of_nonneg ?_
rw [← h]
exact dist_nonneg
have hr0 : s₂.radius - s₁.radius ≠ 0 := by
intro hr0
rw [hr0, dist_eq_zero] at h
exact h0 h.symm
refine ⟨AffineMap.lineMap s₂.center s₁.center (s₂.radius / (s₂.radius - s₁.radius)), ?_, ?_, ?_⟩
· simp only [mem_sphere, dist_lineMap_right, Real.norm_eq_abs, h, one_sub_div hr0, abs_div, sub_sub_cancel_left,
abs_neg, abs_of_nonneg h₁, ha]
field_simp
· simp only [mem_sphere, dist_lineMap_left, norm_div, Real.norm_eq_abs, h, ha, abs_of_nonneg h₂]
field_simp
· rw [wbtw_iff_left_eq_or_right_mem_image_Ici]
simp only [Ne.symm h0, Set.mem_image, Set.mem_Ici, AffineMap.lineMap_eq_lineMap_iff, false_or, exists_eq_right]
rw [one_le_div]
· linarith
· rw [← h]
simp [Ne.symm h0]
