English
The distance from a point to a set equals the distance to its closure: infEdist x (closure s) = infEdist x s.
Русский
Расстояние от x до множества равно расстоянию до его замыкания.
LaTeX
$$$\infEdist x (\overline{s}) = \infEdist x s$$$
Lean4
/-- The edist to a set and to its closure coincide -/
theorem infEdist_closure : infEdist x (closure s) = infEdist x s :=
by
refine le_antisymm (infEdist_anti subset_closure) ?_
refine ENNReal.le_of_forall_pos_le_add fun ε εpos h => ?_
have ε0 : 0 < (ε / 2 : ℝ≥0∞) := by simpa [pos_iff_ne_zero] using εpos
have : infEdist x (closure s) < infEdist x (closure s) + ε / 2 := ENNReal.lt_add_right h.ne ε0.ne'
obtain ⟨y : α, ycs : y ∈ closure s, hy : edist x y < infEdist x (closure s) + ↑ε / 2⟩ := infEdist_lt_iff.mp this
obtain ⟨z : α, zs : z ∈ s, dyz : edist y z < ↑ε / 2⟩ := EMetric.mem_closure_iff.1 ycs (ε / 2) ε0
calc
infEdist x s ≤ edist x z := infEdist_le_edist_of_mem zs
_ ≤ edist x y + edist y z := (edist_triangle _ _ _)
_ ≤ infEdist x (closure s) + ε / 2 + ε / 2 := (add_le_add (le_of_lt hy) (le_of_lt dyz))
_ = infEdist x (closure s) + ↑ε := by rw [add_assoc, ENNReal.add_halves]
