isUniformEmbedding_uniformFunOfFun

English

The map that sends a continuous map f to its evaluation into the space of uniform functions is a uniform embedding.

Русский

Отображение, отправляющее непрерывную отображение f в его представление как элемент пространства UniformFun, является униформным вложением.

LaTeX

$$$\text{IsUniformEmbedding }( (\text{ofFun} \cdot) : C(\alpha, \beta) \to \alpha \to_{\mathsf{u}} \beta)$$$

Lean4

theorem isUniformEmbedding_uniformFunOfFun : IsUniformEmbedding ((ofFun ·) : C(α, β) → α →ᵤ β)
    where
  comap_uniformity :=
    UniformOnFun.uniformEquivUniformFun β _ isCompact_univ |>.isUniformEmbedding.comp
        isUniformEmbedding_toUniformOnFunIsCompact |>.comap_uniformity
  injective := DFunLike.coe_injective

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