extend_exists — Mathlib

English

If s is dense in α, f is uniformly continuous on s, then there exists b with Tendsto f within nhds around a.

Русский

Если s плотное в α, f равномерно непрерывна на s, тогда существует предел b с переходом в nhds вокруг a.

LaTeX

$$$\text{For dense } s \subseteq \alpha,\; \exists b, \ Tendsto\ f\ (\ comap(\uparrow)\ (\nhds a))\ (\nhds b)$$$

Lean4

theorem extend_exists [CompleteSpace β] (hs : Dense s) (hf : UniformContinuous f) (a : α) :
    ∃ b, Tendsto f (comap (↑) (𝓝 a)) (𝓝 b) :=
  uniformly_extend_exists (isUniformInducing_val s) hs.denseRange_val hf a

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