English
The compact convergence uniformity on C(α,β) has a basis indexed by compact subsets and a basis of β's uniformity.
Русский
Униформность компактной сходимости для C(α,β) имеет базис, индексируемый компактными подмножествами и базис равномерности β.
LaTeX
$$$$ HasBasis (\\mathcal{U} C(\\alpha,β)) (\\lambda i. IsCompact i.1) (\\lambda i. {fg : C(α,β) × C(α,β) \\mid \\forall x \\in i.1, (fg.1 x, fg.2 x) \\in i.2}). $$$$
Lean4
theorem _root_.Filter.HasBasis.compactConvergenceUniformity {ι : Type*} {pi : ι → Prop} {s : ι → Set (β × β)}
(h : (𝓤 β).HasBasis pi s) :
HasBasis (𝓤 C(α, β)) (fun p : Set α × ι => IsCompact p.1 ∧ pi p.2) fun p =>
{fg : C(α, β) × C(α, β) | ∀ x ∈ p.1, (fg.1 x, fg.2 x) ∈ s p.2} :=
by
rw [← isUniformEmbedding_toUniformOnFunIsCompact.comap_uniformity]
exact
.comap _ <|
UniformOnFun.hasBasis_uniformity_of_basis _ _ {K | IsCompact K} ⟨∅, isCompact_empty⟩
(directedOn_of_sup_mem fun _ _ ↦ IsCompact.union) h
