dist_eq_of_mem_of_mem — Mathlib

English

For a tangent sphere s and as, the infimum distance from the center to as equals the radius of s.

Русский

Для касательной сферы s и as инфиминальное расстояние от центра до as равно радиусу сферы.

LaTeX

$$$ \\operatorname{Metric.infDist}(s.center, as) = s.radius $$$

Lean4

/-- If two tangent lines to a sphere pass through the same point `q`,
then the distances from `q` to the tangent points are equal. -/
theorem dist_eq_of_mem_of_mem {s : Sphere P} {p₁ p₂ q : P} {as₁ as₂ : AffineSubspace ℝ P} (h₁ : s.IsTangentAt p₁ as₁)
    (h₂ : s.IsTangentAt p₂ as₂) (hq_mem₁ : q ∈ as₁) (hq_mem₂ : q ∈ as₂) : dist q p₁ = dist q p₂ :=
  by
  have h1 := dist_sq_eq_of_mem h₁ hq_mem₁
  have h2 := dist_sq_eq_of_mem h₂ hq_mem₂
  rwa [h1, add_left_cancel_iff, sq_eq_sq₀ dist_nonneg dist_nonneg] at h2

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