exists_mem_closure_infDist_eq_dist

English

Let α be a proper metric space and s ⊆ α with s nonempty. For every x ∈ α, there exists y ∈ closure(s) such that infDist(x, s) = dist(x, y). In words, the distance from x to s is realized by a point in the closure of s.

Русский

Пусть α — корректное метрическое пространство и s ⊆ α непусто. Для каждого x ∈ α существует y ∈ closure(s) такое, что infDist(x, s) = dist(x, y). Иными словами, расстояние от x до s достигается точкой в замыкании s.

LaTeX

$$$\forall s\subseteq\alpha\, (s\neq\varnothing) \Rightarrow \forall x\in\alpha, \exists y \in \overline{s}, \operatorname{infDist}(x,s)=\operatorname{dist}(x,y).$$$

Lean4

theorem exists_mem_closure_infDist_eq_dist [ProperSpace α] (hne : s.Nonempty) (x : α) :
    ∃ y ∈ closure s, infDist x s = dist x y := by
  simpa only [infDist_closure] using isClosed_closure.exists_infDist_eq_dist hne.closure x

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