English
If α is weakly locally compact and σ-compact and the uniformity on β is countably generated, then the uniformity on the function space C(α, β) is also countably generated.
Русский
Пусть α — слабо локально компактное и σ-компактное пространство, а униформность β — счётно порождаемая; тогда униформность на пространстве функций C(α, β) также счётно порождаема.
LaTeX
$$$[\text{WeaklyLocallyCompactSpace } α] \; [\text{SigmaCompactSpace } α] \; [IsCountablyGenerated (\mathcal{U} β)] \Rightarrow IsCountablyGenerated (\mathcal{U} (C(α, β)))$$$
Lean4
/-- If `α` is a weakly locally compact σ-compact space
(e.g., a proper pseudometric space or a compact spaces)
and the uniformity on `β` is pseudometrizable,
then the uniformity on `C(α, β)` is pseudometrizable too.
-/
instance [WeaklyLocallyCompactSpace α] [SigmaCompactSpace α] [IsCountablyGenerated (𝓤 β)] :
IsCountablyGenerated (𝓤 (C(α, β))) :=
let ⟨_V, hV⟩ := exists_antitone_basis (𝓤 β)
((CompactExhaustion.choice α).hasAntitoneBasis_compactConvergenceUniformity hV).isCountablyGenerated
