continuousAt_inv_infDist_pt — Mathlib

English

If x is not in the closure of s, then the map x ↦ (infDist(x,s))^{-1} is continuous at x.

Русский

Если x не в замыкании s, то функция x ↦ (infDist(x,s))^{-1} непрерывна в x.

LaTeX

$$$(x \notin closure(s)) \Rightarrow ContinuousAt ((infDist \cdot s)^{-1}) x$$$

Lean4

theorem continuousAt_inv_infDist_pt (h : x ∉ closure s) : ContinuousAt (fun x ↦ (infDist x s)⁻¹) x :=
  by
  rcases s.eq_empty_or_nonempty with (rfl | hs)
  · simp only [infDist_empty, continuousAt_const]
  · refine (continuous_infDist_pt s).continuousAt.inv₀ ?_
    rwa [Ne, ← mem_closure_iff_infDist_zero hs]

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