exists_infEdist_eq_edist — Mathlib

English

If s is compact and nonempty, then for every x there exists a point y in s such that infEdist x s equals edist x y.

Русский

Если s компактно и непусто, то для каждого x существует y ∈ s с infEdist x s = edist x y.

LaTeX

$$$\forall x\in \alpha,\ \exists y \in s,\ infEdist x s = edist x y$$$

Lean4

theorem _root_.IsCompact.exists_infEdist_eq_edist (hs : IsCompact s) (hne : s.Nonempty) (x : α) :
    ∃ y ∈ s, infEdist x s = edist x y :=
  by
  have A : Continuous fun y => edist x y := continuous_const.edist continuous_id
  obtain ⟨y, ys, hy⟩ := hs.exists_isMinOn hne A.continuousOn
  exact ⟨y, ys, le_antisymm (infEdist_le_edist_of_mem ys) (by rwa [le_infEdist])⟩

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