English
Let α, β be uniform spaces, s ⊆ α with Dense s, and f: s → β be uniformly continuous. If β is a complete space, then the extension of f to α is uniformly continuous.
Русский
Пусть α и β — равномерные пространства, s ⊆ α плотное в α, и f: s → β равномерно непрерывно. Если β является полным пространством, то продолжение f на α является равномерно непрерывным.
LaTeX
$$$$\text{If } (\alpha,\mathcal{U}_{\alpha})\text{ and } (\beta,\mathcal{U}_{\beta})\text{ are uniform spaces } s\subseteq \alpha\text{ is dense},\ f:s\to\beta\text{ is uniform},\ \beta\text{ is complete}, \text{ then } \widehat{f}:=\operatorname{extend}_s(f)\text{ is uniform on }\alpha.$$$$
Lean4
theorem uniformContinuous_extend [CompleteSpace β] (hs : Dense s) (hf : UniformContinuous f) :
UniformContinuous (hs.extend f) :=
uniformContinuous_uniformly_extend (isUniformInducing_val s) hs.denseRange_val hf
