isUniformEmbedding_toUniformOnFunIsCompact

English

There is a basis description for the uniformity on C(α,β) compatible with compact convergence: the basis is indexed by compact subsets and a basis of β's uniformity.

Русский

Существует базисное описание равномерности на C(α,β), совместимое с компактной равномерностью: базис задается компактными подмножествами и базисом равномерности β.

LaTeX

$$$$ HasBasis (\\mathcal{U} C(\\alpha,\\beta)) (\\lambda p. IsCompact p.1 \\land p.2) (\\lambda p. {fg : C(α,β) × C(α,β) \\mid \\forall x \\in p.1, (fg.1 x, fg.2 x) \\in p.2}). $$$$

Lean4

theorem isUniformEmbedding_toUniformOnFunIsCompact :
    IsUniformEmbedding (toUniformOnFunIsCompact : C(α, β) → α →ᵤ[{K | IsCompact K}] β)
    where
  comap_uniformity := rfl
  injective := DFunLike.coe_injective

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