English
For a compact exhaustion K, and a basis hb of β, the compact convergence uniformity on C(α,β) has a basis indexed by (n,i) with i from the basis for β and n from the exhaustion.
Русский
Для компактной исчерпывающей последовательности K и базиса hb для β базис 𝓤 C(α,β) задается индексированный базис по (n,i).
LaTeX
$$$$ HasBasis (𝓤 C(α,β)) (\\lambda i: i.2) (\\lambda i: {fg | ∀ x ∈ i.1, (fg.1 x, fg.2 x) ∈ i.2}). $$$$
Lean4
/-- If `K` is a compact exhaustion of `α`
and `V i` bounded by `p i` is a basis of entourages of `β`,
then `fun (n, i) ↦ {(f, g) | ∀ x ∈ K n, (f x, g x) ∈ V i}` bounded by `p i`
is a basis of entourages of `C(α, β)`. -/
theorem _root_.CompactExhaustion.hasBasis_compactConvergenceUniformity {ι : Type*} {p : ι → Prop} {V : ι → Set (β × β)}
(K : CompactExhaustion α) (hb : (𝓤 β).HasBasis p V) :
HasBasis (𝓤 C(α, β)) (fun i : ℕ × ι ↦ p i.2) fun i ↦ {fg | ∀ x ∈ K i.1, (fg.1 x, fg.2 x) ∈ V i.2} :=
(UniformOnFun.hasBasis_uniformity_of_covering_of_basis {K | IsCompact K} K.isCompact (Monotone.directed_le K.subset)
(fun _ ↦ K.exists_superset_of_isCompact) hb).comap
_
