dist_center — Mathlib

English

If two spheres s1 and s2 are internally tangent, then the distance between centers equals the difference of the radii, i.e., s2 has the larger radius.

Русский

Если сферы s1 и s2 внутренне касаются, расстояние между центрами равно разности радиусов; у второй сферы радиус больше первого.

LaTeX

$$$\operatorname{dist}(s_1.center, s_2.center) = s_2.radius - s_1.radius$$$

Lean4

theorem dist_center {s₁ s₂ : Sphere P} (h : s₁.IsIntTangent s₂) : dist s₁.center s₂.center = s₂.radius - s₁.radius :=
  by
  rcases h with ⟨p, h₁, h₂, h⟩
  rw [← dist_add_dist_eq_iff, mem_sphere'.1 h₁, mem_sphere'.1 h₂] at h
  simp [← h, dist_comm]

Похожие утверждения