radius_le_dist_center — Mathlib

English

If s.IsTangent as, then for all p ∈ as, radius ≤ dist(p, center).

Русский

Если s IsTangent as, то для всех p ∈ as выполняется radius ≤ dist(p, center).

LaTeX

$$$ s.radius \\leq \\mathrm{dist}(p, s.center) $$$

Lean4

theorem radius_le_dist_center {s : Sphere P} {as : AffineSubspace ℝ P} (h : s.IsTangent as) {p : P} (hp : p ∈ as) :
    s.radius ≤ dist p s.center := by
  obtain ⟨x, h⟩ := h
  refine le_of_sq_le_sq ?_ dist_nonneg
  rw [h.dist_sq_eq_of_mem hp, le_add_iff_nonneg_right]
  exact sq_nonneg _

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