English
Let α be a space with a compact exhaustion K = (K_n) and let β be a uniform space with a basis V = (V_n) that is antitone. Then the space C(α, β) of continuous maps carries the compact-convergence uniformity and its uniform structure is generated by the family of sets { (f, g) ∈ C(α, β) × C(α, β) : ∀ x ∈ K_n, (f(x), g(x)) ∈ V_n } as n ranges over ℕ.
Русский
Пусть α — пространство с расходом компактов K = (K_n), β — униформное пространство с анти-монтонной базой V = (V_n). Тогда множество непрерывных отображений C(α, β) оснащено топологией компактной согласованности, и её униформная структура порождается семейством множеств { (f, g) ∈ C(α, β) × C(α, β) : ∀ x ∈ K_n, (f(x), g(x)) ∈ V_n } по переменным n.
LaTeX
$$$\text{HasAntitoneBasis} \, (\mathcal{U} \, C(\alpha, \beta)) \, \big( n \mapsto \{ f g : C(\alpha,\beta) \times C(\alpha,\beta) \mid \forall x \in K_n, (f x, g x) \in V_n\} \big)$$$
Lean4
theorem _root_.CompactExhaustion.hasAntitoneBasis_compactConvergenceUniformity {V : ℕ → Set (β × β)}
(K : CompactExhaustion α) (hb : (𝓤 β).HasAntitoneBasis V) :
HasAntitoneBasis (𝓤 C(α, β)) fun n ↦ {fg | ∀ x ∈ K n, (fg.1 x, fg.2 x) ∈ V n} :=
(UniformOnFun.hasAntitoneBasis_uniformity {K | IsCompact K} K.isCompact K.subset
(fun _ ↦ K.exists_superset_of_isCompact) hb).comap
_
