English
Let s be dense in α, f: s → β uniformly continuous, and a ∈ α. Then the extension hs.extend f a is the limit of f along nets from s converging to a; i.e., Tendsto f (comap (Subtype.val) (nhds a)) (nhds (hs.extend f a)).
Русский
Пусть s плотно в α, f: s → β равномерно непрерывна, и a ∈ α. Тогда продолжение hs.extend f a является пределом f по сетям, стремящимся к a; то есть Tendsto f (comap Subtype.val (nhds a)) (nhds (hs.extend f a)).
LaTeX
$$$$ \\operatorname{Tendsto} f (\\operatorname{comap} (\\mathrm{Subtype.val}) (\\mathcal{N}(a))) (\\mathcal{N}(\\mathrm{hs.extend} f\, a)). $$$$
Lean4
theorem extend_spec [CompleteSpace β] (hs : Dense s) (hf : UniformContinuous f) (a : α) :
Tendsto f (comap (↑) (𝓝 a)) (𝓝 (hs.extend f a)) :=
uniformly_extend_spec (isUniformInducing_val s) hs.denseRange_val hf a
