tendsto_of_uniformContinuous_subtype

English

If f restricted to s is uniformly continuous and a ∈ closure of s, then f tends to f(a) along nhds a.

Русский

Если ограничение f на s равномерно непрерывно и a принадлежит замыканию s, то f стремится к f(a) по nhds a.

LaTeX

$$$$\\text{If } hf: \\mathrm{UniformContinuous}\\; (\\lambda x: f x)\\,|_s \\, \\text{ and } ha: s \\in \\mathcal{N}(a), \\text{ then } \\mathrm{Tendsto}\; f\\; (\\mathcal{N}(a))\\; (\\mathcal{N}(f(a))).$$$$

Lean4

theorem tendsto_of_uniformContinuous_subtype [UniformSpace α] [UniformSpace β] {f : α → β} {s : Set α} {a : α}
    (hf : UniformContinuous fun x : s => f x.val) (ha : s ∈ 𝓝 a) : Tendsto f (𝓝 a) (𝓝 (f a)) :=
  by
  rw [(@map_nhds_subtype_coe_eq_nhds α _ s a (mem_of_mem_nhds ha) ha).symm]
  exact tendsto_map' hf.continuous.continuousAt

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