infDist_eq_radius — Mathlib

English

For a tangent sphere, infDist from center to as equals the radius.

Русский

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

LaTeX

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

Lean4

theorem infDist_eq_radius {s : Sphere P} {as : AffineSubspace ℝ P} (h : s.IsTangent as) :
    Metric.infDist s.center as = s.radius := by
  obtain ⟨p, h⟩ := h
  refine le_antisymm ?_ ?_
  · convert Metric.infDist_le_dist_of_mem h.mem_space
    rw [mem_sphere'.1 h.mem_sphere]
  · rw [Metric.infDist_eq_iInf]
    have : Nonempty as := ⟨⟨p, h.mem_space⟩⟩
    refine le_ciInf fun x ↦ ?_
    rw [dist_comm]
    exact h.isTangent.radius_le_dist_center x.property

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