Compact convergence (uniform convergence on compact sets)

Given a topological space α and a uniform space β (e.g., a metric space or a topological group), the space of continuous maps C(α, β) carries a natural uniform space structure. We define this uniform space structure in this file and also prove its basic properties.

Main definitions

• ContinuousMap.toUniformOnFunIsCompact: natural embedding of C(α, β) into the space α →ᵤ[{K | IsCompact K}] β of all maps α → β with the uniform space structure of uniform convergence on compacts.

• ContinuousMap.compactConvergenceUniformSpace: the UniformSpace structure on C(α, β) induced by the map above.

Main results

• ContinuousMap.mem_compactConvergence_entourage_iff: a characterisation of the entourages of C(α, β).

  The entourages are generated by the following sets. Given K : Set α and V : Set (β × β), let E(K, V) : Set (C(α, β) × C(α, β)) be the set of pairs of continuous functions α → β which are V-close on K: $$ E(K, V) = \{ (f, g) | ∀ (x ∈ K), (f x, g x) ∈ V \}. $$ Then the sets E(K, V) for all compact sets K and all entourages V form a basis of entourages of C(α, β).

  As usual, this basis of entourages provides a basis of neighbourhoods by fixing f, see nhds_basis_uniformity'.

• Filter.HasBasis.compactConvergenceUniformity: a similar statement that uses a basis of entourages of β instead of all entourages. It is useful, e.g., if β is a metric space.

• ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn: a sequence of functions Fₙ in C(α, β) converges in the compact-open topology to some f iff Fₙ converges to f uniformly on each compact subset K of α.

• Topology induced by the uniformity described above agrees with the compact-open topology. This is essentially the same as ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn.

  This fact is not available as a separate theorem. Instead, we override the projection of ContinuousMap.compactConvergenceUniformity to TopologicalSpace to be ContinuousMap.compactOpen and prove that they agree, see Note [forgetful inheritance] and implementation notes below.

• ContinuousMap.tendsto_iff_tendstoLocallyUniformly: on a weakly locally compact space, a sequence of functions Fₙ in C(α, β) converges to some f iff Fₙ converges to f locally uniformly.

• ContinuousMap.tendsto_iff_tendstoUniformly: on a compact space, a sequence of functions Fₙ in C(α, β) converges to some f iff Fₙ converges to f uniformly.

Implementation details

For technical reasons (see Note [forgetful inheritance]), instead of defining a UniformSpace C(α, β) structure and proving in a theorem that it agrees with the compact-open topology, we override the projection right in the definition, so that the resulting instance uses the compact-open topology.

TODO

• Results about uniformly continuous functions γ → C(α, β) and uniform limits of sequences ι → γ → C(α, β).

theorem ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {ι : Type u₃} {p : Filter ι} {F : ι → C(α, β)} {f : C(α, β)} : Filter.Tendsto F p (nhds f) ↔ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun (i : ι) (a : α) => (F i) a) (⇑f) p K

Compact-open topology on C(α, β) agrees with the topology of uniform convergence on compacts: a family of continuous functions F i tends to f in the compact-open topology if and only if the F i tends to f uniformly on all compact sets.

def ContinuousMap.toUniformOnFunIsCompact {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] (f : C(α, β)) : UniformOnFun α β {K : Set α | IsCompact K}

Interpret a bundled continuous map as an element of α →ᵤ[{K | IsCompact K}] β.

We use this map to induce the UniformSpace structure on C(α, β).

Equations

• f.toUniformOnFunIsCompact = (UniformOnFun.ofFun {K : Set α | IsCompact K}) ⇑f

@[simp]

theorem ContinuousMap.toUniformOnFun_toFun {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] (f : C(α, β)) : (UniformOnFun.toFun {K : Set α | IsCompact K}) f.toUniformOnFunIsCompact = ⇑f

theorem ContinuousMap.range_toUniformOnFunIsCompact {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] : Set.range toUniformOnFunIsCompact = {f : UniformOnFun α β {K : Set α | IsCompact K} | Continuous f}

instance ContinuousMap.compactConvergenceUniformSpace {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] : UniformSpace C(α, β)

Uniform space structure on C(α, β).

The uniformity comes from α →ᵤ[{K | IsCompact K}] β (i.e., UniformOnFun α β {K | IsCompact K}) which defines topology of uniform convergence on compact sets. We use ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn to show that the induced topology agrees with the compact-open topology and replace the topology with compactOpen to avoid non-defeq diamonds, see Note [forgetful inheritance].

Equations

• ContinuousMap.compactConvergenceUniformSpace = (UniformSpace.comap ContinuousMap.toUniformOnFunIsCompact inferInstance).replaceTopology ⋯

theorem ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] : IsUniformEmbedding toUniformOnFunIsCompact

theorem ContinuousMap.continuous_iff_continuous_uniformOnFun {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {X : Type u_1} [TopologicalSpace X] (f : X → C(α, β)) : Continuous f ↔ Continuous fun (x : X) => (UniformOnFun.ofFun {K : Set α | IsCompact K}) ⇑(f x)

f : X → C(α, β) is continuous if any only if it is continuous when reinterpreted as a map f : X → α →ᵤ[{K | IsCompact K}] β.

theorem Filter.HasBasis.compactConvergenceUniformity {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {ι : Type u_1} {pi : ι → Prop} {s : ι → Set (β × β)} (h : (uniformity β).HasBasis pi s) : (uniformity C(α, β)).HasBasis (fun (p : Set α × ι) => IsCompact p.1 ∧ pi p.2) fun (p : Set α × ι) => {fg : C(α, β) × C(α, β) | ∀ x ∈ p.1, (fg.1 x, fg.2 x) ∈ s p.2}

theorem ContinuousMap.hasBasis_compactConvergenceUniformity {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] : (uniformity C(α, β)).HasBasis (fun (p : Set α × Set (β × β)) => IsCompact p.1 ∧ p.2 ∈ uniformity β) fun (p : Set α × Set (β × β)) => {fg : C(α, β) × C(α, β) | ∀ x ∈ p.1, (fg.1 x, fg.2 x) ∈ p.2}

theorem ContinuousMap.mem_compactConvergence_entourage_iff {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] (X : Set (C(α, β) × C(α, β))) : X ∈ uniformity C(α, β) ↔ ∃ (K : Set α) (V : Set (β × β)), IsCompact K ∧ V ∈ uniformity β ∧ {fg : C(α, β) × C(α, β) | ∀ x ∈ K, (fg.1 x, fg.2 x) ∈ V} ⊆ X

theorem CompactExhaustion.hasBasis_compactConvergenceUniformity {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {ι : Type u_1} {p : ι → Prop} {V : ι → Set (β × β)} (K : CompactExhaustion α) (hb : (uniformity β).HasBasis p V) : (uniformity C(α, β)).HasBasis (fun (i : ℕ × ι) => p i.2) fun (i : ℕ × ι) => {fg : C(α, β) × C(α, β) | ∀ x ∈ K i.1, (fg.1 x, fg.2 x) ∈ V i.2}

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 CompactExhaustion.hasAntitoneBasis_compactConvergenceUniformity {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {V : ℕ → Set (β × β)} (K : CompactExhaustion α) (hb : (uniformity β).HasAntitoneBasis V) : (uniformity C(α, β)).HasAntitoneBasis fun (n : ℕ) => {fg : C(α, β) × C(α, β) | ∀ x ∈ K n, (fg.1 x, fg.2 x) ∈ V n}

instance ContinuousMap.instIsCountablyGeneratedProdUniformityOfWeaklyLocallyCompactSpaceOfSigmaCompactSpace {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] [WeaklyLocallyCompactSpace α] [SigmaCompactSpace α] [(uniformity β).IsCountablyGenerated] : (uniformity C(α, β)).IsCountablyGenerated

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.

theorem ContinuousMap.tendsto_of_tendstoLocallyUniformly {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {f : C(α, β)} {ι : Type u₃} {p : Filter ι} {F : ι → C(α, β)} (h : TendstoLocallyUniformly (fun (i : ι) (a : α) => (F i) a) (⇑f) p) : Filter.Tendsto F p (nhds f)

Locally uniform convergence implies convergence in the compact-open topology.

theorem ContinuousMap.tendsto_iff_tendstoLocallyUniformly {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {f : C(α, β)} {ι : Type u₃} {p : Filter ι} {F : ι → C(α, β)} [WeaklyLocallyCompactSpace α] : Filter.Tendsto F p (nhds f) ↔ TendstoLocallyUniformly (fun (i : ι) (a : α) => (F i) a) (⇑f) p

In a weakly locally compact space, convergence in the compact-open topology is the same as locally uniform convergence.

The right-to-left implication holds in any topological space, see ContinuousMap.tendsto_of_tendstoLocallyUniformly.

theorem ContinuousMap.uniformContinuous_comp {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {δ : Type u_2} [UniformSpace δ] (g : C(β, δ)) (hg : UniformContinuous ⇑g) : UniformContinuous g.comp

theorem ContinuousMap.isUniformInducing_comp {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {δ : Type u_2} [UniformSpace δ] (g : C(β, δ)) (hg : IsUniformInducing ⇑g) : IsUniformInducing g.comp

theorem ContinuousMap.isUniformEmbedding_comp {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {δ : Type u_2} [UniformSpace δ] (g : C(β, δ)) (hg : IsUniformEmbedding ⇑g) : IsUniformEmbedding g.comp

theorem ContinuousMap.uniformContinuous_comp_left {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {γ : Type u_1} [TopologicalSpace γ] (g : C(α, γ)) : UniformContinuous fun (f : C(γ, β)) => f.comp g

def UniformEquiv.arrowCongr {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {γ : Type u_1} {δ : Type u_2} [TopologicalSpace γ] [UniformSpace δ] (φ : α ≃ₜ γ) (ψ : β ≃ᵤ δ) : C(α, β) ≃ᵤ C(γ, δ)

Any pair of a homeomorphism X ≃ₜ Z and an isomorphism Y ≃ᵤ T of uniform spaces gives rise to an isomorphism C(X, Y) ≃ᵤ C(Z, T).

Equations

• One or more equations did not get rendered due to their size.

theorem ContinuousMap.hasBasis_compactConvergenceUniformity_of_compact {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] [CompactSpace α] : (uniformity C(α, β)).HasBasis (fun (V : Set (β × β)) => V ∈ uniformity β) fun (V : Set (β × β)) => {fg : C(α, β) × C(α, β) | ∀ (x : α), (fg.1 x, fg.2 x) ∈ V}

theorem Filter.HasBasis.compactConvergenceUniformity_of_compact {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] [CompactSpace α] {ι : Sort u_1} {p : ι → Prop} {V : ι → Set (β × β)} (h : (uniformity β).HasBasis p V) : (uniformity C(α, β)).HasBasis p fun (i : ι) => {fg : C(α, β) × C(α, β) | ∀ (x : α), (fg.1 x, fg.2 x) ∈ V i}

theorem ContinuousMap.isUniformEmbedding_uniformFunOfFun {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] [CompactSpace α] : IsUniformEmbedding fun (x : C(α, β)) => UniformFun.ofFun ⇑x

theorem ContinuousMap.tendsto_iff_tendstoUniformly {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {f : C(α, β)} {ι : Type u₃} {p : Filter ι} {F : ι → C(α, β)} [CompactSpace α] : Filter.Tendsto F p (nhds f) ↔ TendstoUniformly (fun (i : ι) (a : α) => (F i) a) (⇑f) p

Convergence in the compact-open topology is the same as uniform convergence for sequences of continuous functions on a compact space.

theorem ContinuousMap.continuous_iff_continuous_uniformFun {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] [CompactSpace α] {X : Type u_1} [TopologicalSpace X] (f : X → C(α, β)) : Continuous f ↔ Continuous fun (x : X) => UniformFun.ofFun ⇑(f x)

When α is compact, f : X → C(α, β) is continuous if any only if it is continuous when reinterpreted as a map f : X → α →ᵤ β.

theorem ContinuousOn.tendsto_restrict_iff_tendstoUniformlyOn {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {s : Set α} [CompactSpace ↑s] {f : α → β} (hf : ContinuousOn f s) {ι : Type u_1} {p : Filter ι} {F : ι → α → β} (hF : ∀ (i : ι), ContinuousOn (F i) s) : Filter.Tendsto (fun (i : ι) => { toFun := s.restrict (F i), continuous_toFun := ⋯ }) p (nhds { toFun := s.restrict f, continuous_toFun := ⋯ }) ↔ TendstoUniformlyOn F f p s

Given functions F i, f which are continuous on a compact set s, F tends to f uniformly on s if and only if the restrictions (as elements of C(s, β)) converge.

theorem ContinuousOn.continuous_restrict_iff_continuous_uniformOnFun {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {X : Type u_1} [TopologicalSpace X] {f : X → α → β} {s : Set α} (hf : ∀ (x : X), ContinuousOn (f x) s) [CompactSpace ↑s] : (Continuous fun (x : X) => { toFun := s.restrict (f x), continuous_toFun := ⋯ }) ↔ Continuous fun (x : X) => (UniformOnFun.ofFun {s}) (f x)

A family f : X → α → β, each of which is continuous on a compact set s : Set α is continuous in the topology X → α →ᵤ[{s}] β if and only if the family of continuous restrictions X → C(s, β) is continuous.

theorem ContinuousMap.uniformSpace_eq_inf_precomp_of_cover {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {δ₁ : Type u_1} {δ₂ : Type u_2} [TopologicalSpace δ₁] [TopologicalSpace δ₂] (φ₁ : C(δ₁, α)) (φ₂ : C(δ₂, α)) (h_proper₁ : IsProperMap ⇑φ₁) (h_proper₂ : IsProperMap ⇑φ₂) (h_cover : Set.range ⇑φ₁ ∪ Set.range ⇑φ₂ = Set.univ) : inferInstanceAs (UniformSpace C(α, β)) = UniformSpace.comap (fun (x : C(α, β)) => x.comp φ₁) inferInstance ⊓ UniformSpace.comap (fun (x : C(α, β)) => x.comp φ₂) inferInstance

theorem ContinuousMap.uniformSpace_eq_iInf_precomp_of_cover {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {ι : Type u₃} {δ : ι → Type u_1} [(i : ι) → TopologicalSpace (δ i)] (φ : (i : ι) → C(δ i, α)) (h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)) (h_lf : LocallyFinite fun (i : ι) => Set.range ⇑(φ i)) (h_cover : ⋃ (i : ι), Set.range ⇑(φ i) = Set.univ) : inferInstanceAs (UniformSpace C(α, β)) = ⨅ (i : ι), UniformSpace.comap (fun (x : C(α, β)) => x.comp (φ i)) inferInstance

instance ContinuousMap.instCompleteSpaceOfCompactlyCoherentSpace {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] [CompleteSpace β] [CompactlyCoherentSpace α] : CompleteSpace C(α, β)

If the topology on α is generated by its restrictions to compact sets, then the space of continuous maps C(α, β) is complete (w.r.t. the compact convergence uniformity).

Sufficient conditions on α to satisfy this condition are (weak) local compactness and sequential compactness.

@[deprecated ContinuousMap.instCompleteSpaceOfCompactlyCoherentSpace (since := "2025-06-03")]

theorem ContinuousMap.completeSpace_of_isCoherentWith {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] [CompleteSpace β] [CompactlyCoherentSpace α] : CompleteSpace C(α, β)

Alias of ContinuousMap.instCompleteSpaceOfCompactlyCoherentSpace.

---

If the topology on α is generated by its restrictions to compact sets, then the space of continuous maps C(α, β) is complete (w.r.t. the compact convergence uniformity).

Sufficient conditions on α to satisfy this condition are (weak) local compactness and sequential compactness.

@[deprecated ContinuousMap.instCompleteSpaceOfCompactlyCoherentSpace (since := "2025-04-08")]

theorem ContinuousMap.completeSpace_of_restrictGenTopology {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] [CompleteSpace β] [CompactlyCoherentSpace α] : CompleteSpace C(α, β)

Alias of ContinuousMap.instCompleteSpaceOfCompactlyCoherentSpace.

---

If the topology on α is generated by its restrictions to compact sets, then the space of continuous maps C(α, β) is complete (w.r.t. the compact convergence uniformity).

Sufficient conditions on α to satisfy this condition are (weak) local compactness and sequential compactness.

theorem ContinuousMap.isComplete_setOf_eqOn {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] [CompleteSpace C(α, β)] (f : α → β) (s : Set α) : IsComplete {g : C(α, β) | Set.EqOn (⇑g) f s}

If C(α, β) is a complete space, then for any (possibly, discontinuous) function f and any set s, the set of functions g : C(α, β) that are equal to f on s is a complete set.

Note that this set does not have to be a closed set when β is not T0. This lemma is useful to prove that, e.g., the space of paths between two points and the space of homotopies between two continuous maps are complete spaces, without assuming that the codomain is a Hausdorff space.