dist_center — Mathlib

English

If two spheres s1 and s2 are externally tangent, then the distance between their centers equals the sum of their radii.

Русский

Если две сферы s1 и s2 внешне касаются, то расстояние между их центрами равно сумме их радиусов.

LaTeX

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

Lean4

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

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