exists_infDist_eq_dist — Mathlib

English

For a nonempty compact set s and any x, there exists y ∈ s with infDist x s = dist x y.

Русский

Для непустого компактного множества s и любого x существует y ∈ s такое, что infDist x s = dist x y.

LaTeX

$$IsCompact s → s.Nonempty → ∀ x, ∃ y ∈ s, infDist x s = dist x y$$

Lean4

theorem _root_.IsCompact.exists_infDist_eq_dist (h : IsCompact s) (hne : s.Nonempty) (x : α) :
    ∃ y ∈ s, infDist x s = dist x y :=
  let ⟨y, hys, hy⟩ := h.exists_infEdist_eq_edist hne x
  ⟨y, hys, by rw [infDist, dist_edist, hy]⟩

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