# mathlib3documentation

topology.uniform_space.compact_convergence

# Compact convergence (uniform convergence on compact sets) #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 the following properties of the topology it induces on C(α, β):

1. Given a sequence of continuous functions Fₙ : α → β together with some continuous f : α → β, then Fₙ converges to f as a sequence in C(α, β) iff Fₙ converges to f uniformly on each compact subset K of α.
2. Given Fₙ and f as above and suppose α is locally compact, then Fₙ converges to f iff Fₙ converges to f locally uniformly.
3. The topology coincides with the compact-open topology.

Property 1 is essentially true by definition, 2 follows from basic results about uniform convergence, but 3 requires a little work and uses the Lebesgue number lemma.

## The uniform space structure #

Given subsets K ⊆ α and V ⊆ β × β, let E(K, V) ⊆ 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 \}.$$ Fixing some f ∈ C(α, β), let N(K, V, f) ⊆ C(α, β) be the set of continuous functions α → β which are V-close to f on K: $$N(K, V, f) = \{ g | ∀ (x ∈ K), (f x, g x) ∈ V \}.$$ Using this notation we can describe the uniform space structure and the topology it induces. Specifically:

• A subset X ⊆ C(α, β) × C(α, β) is an entourage for the uniform space structure on C(α, β) iff there exists a compact K and entourage V such that E(K, V) ⊆ X.
• A subset Y ⊆ C(α, β) is a neighbourhood of f iff there exists a compact K and entourage V such that N(K, V, f) ⊆ Y.

The topology on C(α, β) thus has a natural subbasis (the compact-open subbasis) and a natural neighbourhood basis (the compact-convergence neighbourhood basis).

## Main definitions / results #

• compact_open_eq_compact_convergence: the compact-open topology is equal to the compact-convergence topology.
• compact_convergence_uniform_space: the uniform space structure on C(α, β).
• mem_compact_convergence_entourage_iff: a characterisation of the entourages of C(α, β).
• tendsto_iff_forall_compact_tendsto_uniformly_on: a sequence of functions Fₙ in C(α, β) converges to some f iff Fₙ converges to f uniformly on each compact subset K of α.
• tendsto_iff_tendsto_locally_uniformly: on a locally compact space, a sequence of functions Fₙ in C(α, β) converges to some f iff Fₙ converges to f locally uniformly.
• tendsto_iff_tendsto_uniformly: on a compact space, a sequence of functions Fₙ in C(α, β) converges to some f iff Fₙ converges to f uniformly.

## Implementation details #

We use the forgetful inheritance pattern (see Note [forgetful inheritance]) to make the topology of the uniform space structure on C(α, β) definitionally equal to the compact-open topology.

## TODO #

• When β is a metric space, there is natural basis for the compact-convergence topology parameterised by triples (K, ε, f) for a real number ε > 0.
• When α is compact and β is a metric space, the compact-convergence topology (and thus also the compact-open topology) is metrisable.
• Results about uniformly continuous functions γ → C(α, β) and uniform limits of sequences ι → γ → C(α, β).
def continuous_map.compact_conv_nhd {α : Type u₁} {β : Type u₂} (K : set α) (V : set × β)) (f : C(α, β)) :
set C(α, β)

Given K ⊆ α, V ⊆ β × β, and f : C(α, β), we define compact_conv_nhd K V f to be the set of g : C(α, β) that are V-close to f on K.

Equations
theorem continuous_map.self_mem_compact_conv_nhd {α : Type u₁} {β : Type u₂} {K : set α} {V : set × β)} (f : C(α, β)) (hV : V ) :
theorem continuous_map.compact_conv_nhd_mono {α : Type u₁} {β : Type u₂} {K : set α} {V : set × β)} (f : C(α, β)) {V' : set × β)} (hV' : V' V) :
theorem continuous_map.compact_conv_nhd_mem_comp {α : Type u₁} {β : Type u₂} {K : set α} {V : set × β)} (f : C(α, β)) {g₁ g₂ : C(α, β)} {V' : set × β)} (hg₁ : g₁ ) (hg₂ : g₂ ) :
g₂ f
theorem continuous_map.compact_conv_nhd_nhd_basis {α : Type u₁} {β : Type u₂} {K : set α} {V : set × β)} (f : C(α, β)) (hV : V ) :
(V' : set × β)) (H : V' , V' V (g : C(α, β)), g

A key property of compact_conv_nhd. It allows us to apply topological_space.nhds_mk_of_nhds_filter_basis below.

theorem continuous_map.compact_conv_nhd_subset_inter {α : Type u₁} {β : Type u₂} (f : C(α, β)) (K₁ K₂ : set α) (V₁ V₂ : set × β)) :
continuous_map.compact_conv_nhd (K₁ K₂) (V₁ V₂) f
theorem continuous_map.compact_conv_nhd_compact_entourage_nonempty {α : Type u₁} {β : Type u₂}  :
{KV : set α × set × β) | KV.snd .nonempty
theorem continuous_map.compact_conv_nhd_filter_is_basis {α : Type u₁} {β : Type u₂} (f : C(α, β)) :
filter.is_basis (λ (KV : set α × set × β)), KV.snd (λ (KV : set α × set × β)), f)
def continuous_map.compact_convergence_filter_basis {α : Type u₁} {β : Type u₂} (f : C(α, β)) :

A filter basis for the neighbourhood filter of a point in the compact-convergence topology.

Equations
theorem continuous_map.mem_compact_convergence_nhd_filter {α : Type u₁} {β : Type u₂} (f : C(α, β)) (Y : set C(α, β)) :
(K : set α) (V : set × β)) (hK : (hV : V ,
def continuous_map.compact_convergence_topology {α : Type u₁} {β : Type u₂}  :

The compact-convergence topology. In fact, see compact_open_eq_compact_convergence this is the same as the compact-open topology. This definition is thus an auxiliary convenience definition and is unlikely to be of direct use.

Equations
theorem continuous_map.nhds_compact_convergence {α : Type u₁} {β : Type u₂} (f : C(α, β)) :
theorem continuous_map.has_basis_nhds_compact_convergence {α : Type u₁} {β : Type u₂} (f : C(α, β)) :
(nhds f).has_basis (λ (p : set α × set × β)), p.snd (λ (p : set α × set × β)),
theorem continuous_map.tendsto_iff_forall_compact_tendsto_uniformly_on' {α : Type u₁} {β : Type u₂} (f : C(α, β)) {ι : Type u₃} {p : filter ι} {F : ι C(α, β)} :
(nhds f) (K : set α), tendsto_uniformly_on (λ (i : ι) (a : α), (F i) a) f p K

This is an auxiliary lemma and is unlikely to be of direct use outside of this file. See tendsto_iff_forall_compact_tendsto_uniformly_on below for the useful version where the topology is picked up via typeclass inference.

theorem continuous_map.compact_conv_nhd_subset_compact_open {α : Type u₁} {β : Type u₂} {K : set α} (f : C(α, β)) (hK : is_compact K) {U : set β} (hU : is_open U) (hf : f ) :
(V : set × β)) (H : V ,

Any point of compact_open.gen K U is also an interior point wrt the topology of compact convergence.

The topology of compact convergence is thus at least as fine as the compact-open topology.

theorem continuous_map.Inter_compact_open_gen_subset_compact_conv_nhd {α : Type u₁} {β : Type u₂} {K : set α} {V : set × β)} (f : C(α, β)) (hK : is_compact K) (hV : V ) :
(ι : Type u₁) [_inst_3 : fintype ι] (C : ι set α) (hC : (i : ι), is_compact (C i)) (U : ι set β) (hU : (i : ι), is_open (U i)), (f (i : ι), (U i)) ( (i : ι), (U i))

The point f in compact_conv_nhd K V f is also an interior point wrt the compact-open topology.

Since compact_conv_nhd K V f are a neighbourhood basis at f for each f, it follows that the compact-open topology is at least as fine as the topology of compact convergence.

The compact-open topology is equal to the compact-convergence topology.

def continuous_map.compact_convergence_uniformity {α : Type u₁} {β : Type u₂}  :
filter (C(α, β) × C(α, β))

The filter on C(α, β) × C(α, β) which underlies the uniform space structure on C(α, β).

Equations
theorem continuous_map.has_basis_compact_convergence_uniformity_aux {α : Type u₁} {β : Type u₂}  :
continuous_map.compact_convergence_uniformity.has_basis (λ (p : set α × set × β)), p.snd (λ (p : set α × set × β)), {fg : C(α, β) × C(α, β) | (x : α), x p.fst ((fg.fst) x, (fg.snd) x) p.snd})
theorem continuous_map.mem_compact_convergence_uniformity {α : Type u₁} {β : Type u₂} (X : set (C(α, β) × C(α, β))) :
(K : set α) (V : set × β)) (hK : (hV : V , {fg : C(α, β) × C(α, β) | (x : α), x K ((fg.fst) x, (fg.snd) x) V} X

An intermediate lemma. Usually mem_compact_convergence_entourage_iff is more useful.

@[protected, instance]

Note that we ensure the induced topology is definitionally the compact-open topology.

Equations
theorem continuous_map.mem_compact_convergence_entourage_iff {α : Type u₁} {β : Type u₂} (X : set (C(α, β) × C(α, β))) :
X (K : set α) (V : set × β)) (hK : (hV : V , {fg : C(α, β) × C(α, β) | (x : α), x K ((fg.fst) x, (fg.snd) x) V} X
theorem continuous_map.has_basis_compact_convergence_uniformity {α : Type u₁} {β : Type u₂}  :
(uniformity C(α, β)).has_basis (λ (p : set α × set × β)), p.snd (λ (p : set α × set × β)), {fg : C(α, β) × C(α, β) | (x : α), x p.fst ((fg.fst) x, (fg.snd) x) p.snd})
theorem filter.has_basis.compact_convergence_uniformity {α : Type u₁} {β : Type u₂} {ι : Type u_1} {pi : ι Prop} {s : ι set × β)} (h : (uniformity β).has_basis pi s) :
(uniformity C(α, β)).has_basis (λ (p : set α × ι), pi p.snd) (λ (p : set α × ι), {fg : C(α, β) × C(α, β) | (x : α), x p.fst ((fg.fst) x, (fg.snd) x) s p.snd})
theorem continuous_map.tendsto_iff_forall_compact_tendsto_uniformly_on {α : Type u₁} {β : Type u₂} {f : C(α, β)} {ι : Type u₃} {p : filter ι} {F : ι C(α, β)} :
(nhds f) (K : set α), tendsto_uniformly_on (λ (i : ι) (a : α), (F i) a) f p K
theorem continuous_map.tendsto_of_tendsto_locally_uniformly {α : Type u₁} {β : Type u₂} {f : C(α, β)} {ι : Type u₃} {p : filter ι} {F : ι C(α, β)} (h : tendsto_locally_uniformly (λ (i : ι) (a : α), (F i) a) f p) :
(nhds f)

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

theorem continuous_map.tendsto_locally_uniformly_of_tendsto {α : Type u₁} {β : Type u₂} {f : C(α, β)} {ι : Type u₃} {p : filter ι} {F : ι C(α, β)} (hα : (x : α), (n : set α), n nhds x) (h : (nhds f)) :
tendsto_locally_uniformly (λ (i : ι) (a : α), (F i) a) f p

If every point has a compact neighbourhood, then convergence in the compact-open topology implies locally uniform convergence.

See also tendsto_iff_tendsto_locally_uniformly, especially for T2 spaces.

theorem continuous_map.tendsto_iff_tendsto_locally_uniformly {α : Type u₁} {β : Type u₂} {f : C(α, β)} {ι : Type u₃} {p : filter ι} {F : ι C(α, β)}  :
(nhds f) tendsto_locally_uniformly (λ (i : ι) (a : α), (F i) a) f p

Convergence in the compact-open topology is the same as locally uniform convergence on a locally compact space.

For non-T2 spaces, the assumption locally_compact_space α is stronger than we need and in fact the ← direction is true unconditionally. See tendsto_locally_uniformly_of_tendsto and tendsto_of_tendsto_locally_uniformly for versions requiring weaker hypotheses.

theorem continuous_map.has_basis_compact_convergence_uniformity_of_compact {α : Type u₁} {β : Type u₂}  :
(uniformity C(α, β)).has_basis (λ (V : set × β)), V (λ (V : set × β)), {fg : C(α, β) × C(α, β) | (x : α), ((fg.fst) x, (fg.snd) x) V})
theorem continuous_map.tendsto_iff_tendsto_uniformly {α : Type u₁} {β : Type u₂} {f : C(α, β)} {ι : Type u₃} {p : filter ι} {F : ι C(α, β)}  :
(nhds f) tendsto_uniformly (λ (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.