# Documentation

Mathlib.Topology.CompactOpen

# The compact-open topology #

In this file, we define the compact-open topology on the set of continuous maps between two topological spaces.

## Main definitions #

• CompactOpen is the compact-open topology on C(α, β). It is declared as an instance.
• ContinuousMap.coev is the coevaluation map β → C(α, β × α). It is always continuous.
• ContinuousMap.curry is the currying map C(α × β, γ) → C(α, C(β, γ)). This map always exists and it is continuous as long as α × β is locally compact.
• ContinuousMap.uncurry is the uncurrying map C(α, C(β, γ)) → C(α × β, γ). For this map to exist, we need β to be locally compact. If α is also locally compact, then this map is continuous.
• Homeomorph.curry combines the currying and uncurrying operations into a homeomorphism C(α × β, γ) ≃ₜ C(α, C(β, γ)). This homeomorphism exists if α and β are locally compact.

## Tags #

compact-open, curry, function space

def ContinuousMap.CompactOpen.gen {α : Type u_1} {β : Type u_2} [] [] (s : Set α) (u : Set β) :
Set C(α, β)

A generating set for the compact-open topology (when s is compact and u is open).

Instances For
@[simp]
theorem ContinuousMap.gen_empty {α : Type u_1} {β : Type u_2} [] [] (u : Set β) :
= Set.univ
@[simp]
theorem ContinuousMap.gen_univ {α : Type u_1} {β : Type u_2} [] [] (s : Set α) :
ContinuousMap.CompactOpen.gen s Set.univ = Set.univ
@[simp]
theorem ContinuousMap.gen_inter {α : Type u_1} {β : Type u_2} [] [] (s : Set α) (u : Set β) (v : Set β) :
@[simp]
theorem ContinuousMap.gen_union {α : Type u_1} {β : Type u_2} [] [] (s : Set α) (t : Set α) (u : Set β) :
theorem ContinuousMap.gen_empty_right {α : Type u_1} {β : Type u_2} [] [] {s : Set α} (h : ) :
instance ContinuousMap.compactOpen {α : Type u_1} {β : Type u_2} [] [] :
theorem ContinuousMap.compactOpen_eq {α : Type u_1} {β : Type u_2} [] [] :
ContinuousMap.compactOpen = TopologicalSpace.generateFrom (Set.image2 ContinuousMap.CompactOpen.gen {s | } {t | })

Definition of ContinuousMap.compactOpen in terms of Set.image2.

theorem ContinuousMap.isOpen_gen {α : Type u_1} {β : Type u_2} [] [] {s : Set α} (hs : ) {u : Set β} (hu : ) :
theorem ContinuousMap.continuous_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (g : C(β, γ)) :

C(α, -) is a functor.

theorem ContinuousMap.inducing_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (g : C(β, γ)) (hg : Inducing g) :

If g : C(β, γ) is a topology inducing map, then the composition ContinuousMap.comp g : C(α, β) → C(α, γ) is a topology inducing map too.

theorem ContinuousMap.embedding_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (g : C(β, γ)) (hg : ) :

If g : C(β, γ) is a topological embedding, then the composition ContinuousMap.comp g : C(α, β) → C(α, γ) is an embedding too.

theorem ContinuousMap.continuous_comp_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : C(α, β)) :
Continuous fun g =>

C(-, γ) is a functor.

theorem ContinuousMap.continuous_comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] :
Continuous fun x => ContinuousMap.comp x.snd x.fst

Composition is a continuous map from C(α, β) × C(β, γ) to C(α, γ), provided that β is locally compact. This is Prop. 9 of Chap. X, §3, №. 4 of Bourbaki's Topologie Générale.

theorem ContinuousMap.continuous.comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {X : Type u_4} [] {f : XC(α, β)} {g : XC(β, γ)} (hf : ) (hg : ) :
Continuous fun x => ContinuousMap.comp (g x) (f x)
theorem ContinuousMap.continuous_eval' {α : Type u_1} {β : Type u_2} [] [] :
Continuous fun p => p.fst p.snd

The evaluation map C(α, β) × α → β is continuous if α is locally compact.

See also ContinuousMap.continuous_eval

theorem ContinuousMap.continuous_eval_const {α : Type u_1} {β : Type u_2} [] [] (a : α) :
Continuous fun f => f a

Evaluation of a continuous map f at a point a is continuous in f.

Porting note: merged continuous_eval_const with continuous_eval_const' removing unneeded assumptions.

theorem ContinuousMap.continuous_coe {α : Type u_1} {β : Type u_2} [] [] :
Continuous FunLike.coe

Coercion from C(α, β) with compact-open topology to α → β with pointwise convergence topology is a continuous map.

Porting note: merged continuous_coe with continuous_coe' removing unneeded assumptions.

instance ContinuousMap.instT0SpaceContinuousMapCompactOpen {α : Type u_1} {β : Type u_2} [] [] [] :
instance ContinuousMap.instT1SpaceContinuousMapCompactOpen {α : Type u_1} {β : Type u_2} [] [] [] :
instance ContinuousMap.instT2SpaceContinuousMapCompactOpen {α : Type u_1} {β : Type u_2} [] [] [] :
theorem ContinuousMap.compactOpen_le_induced {α : Type u_1} {β : Type u_2} [] [] (s : Set α) :
ContinuousMap.compactOpen TopologicalSpace.induced () ContinuousMap.compactOpen
theorem ContinuousMap.compactOpen_eq_sInf_induced {α : Type u_1} {β : Type u_2} [] [] :
ContinuousMap.compactOpen = ⨅ (s : Set α) (_ : ), TopologicalSpace.induced () ContinuousMap.compactOpen

The compact-open topology on C(α, β) is equal to the infimum of the compact-open topologies on C(s, β) for s a compact subset of α. The key point of the proof is that the union of the compact subsets of α is equal to the union of compact subsets of the compact subsets of α.

theorem ContinuousMap.continuous_restrict {α : Type u_1} {β : Type u_2} [] [] (s : Set α) :
Continuous fun F =>

For any subset s of α, the restriction of continuous functions to s is continuous as a function from C(α, β) to C(s, β) with their respective compact-open topologies.

theorem ContinuousMap.nhds_compactOpen_eq_sInf_nhds_induced {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) :
nhds f = ⨅ (s : Set α) (_ : ),
theorem ContinuousMap.tendsto_compactOpen_restrict {α : Type u_1} {β : Type u_2} [] [] {ι : Type u_4} {l : } {F : ιC(α, β)} {f : C(α, β)} (hFf : Filter.Tendsto F l (nhds f)) (s : Set α) :
Filter.Tendsto (fun i => ContinuousMap.restrict s (F i)) l ()
theorem ContinuousMap.tendsto_compactOpen_iff_forall {α : Type u_1} {β : Type u_2} [] [] {ι : Type u_4} {l : } (F : ιC(α, β)) (f : C(α, β)) :
Filter.Tendsto F l (nhds f) ∀ (s : Set α), Filter.Tendsto (fun i => ContinuousMap.restrict s (F i)) l ()
theorem ContinuousMap.exists_tendsto_compactOpen_iff_forall {α : Type u_1} {β : Type u_2} [] [] [] {ι : Type u_4} {l : } [] (F : ιC(α, β)) :
(f, Filter.Tendsto F l (nhds f)) ∀ (s : Set α), f, Filter.Tendsto (fun i => ContinuousMap.restrict s (F i)) l (nhds f)

A family F of functions in C(α, β) converges in the compact-open topology, if and only if it converges in the compact-open topology on each compact subset of α.

def ContinuousMap.coev (α : Type u_1) (β : Type u_2) [] [] (b : β) :
C(α, β × α)

The coevaluation map β → C(α, β × α) sending a point x : β to the continuous function on α sending y to (x, y).

Instances For
theorem ContinuousMap.image_coev {α : Type u_1} {β : Type u_2} [] [] {y : β} (s : Set α) :
↑() '' s = {y} ×ˢ s
theorem ContinuousMap.continuous_coev {α : Type u_1} {β : Type u_2} [] [] :
def ContinuousMap.curry' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : C(α × β, γ)) (a : α) :
C(β, γ)

Auxiliary definition, see ContinuousMap.curry and Homeomorph.curry.

Instances For
theorem ContinuousMap.continuous_curry' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : C(α × β, γ)) :

If a map α × β → γ is continuous, then its curried form α → C(β, γ) is continuous.

theorem ContinuousMap.continuous_of_continuous_uncurry {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : αC(β, γ)) (h : Continuous (Function.uncurry fun x y => ↑(f x) y)) :

To show continuity of a map α → C(β, γ), it suffices to show that its uncurried form α × β → γ is continuous.

def ContinuousMap.curry {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : C(α × β, γ)) :
C(α, C(β, γ))

The curried form of a continuous map α × β → γ as a continuous map α → C(β, γ). If a × β is locally compact, this is continuous. If α and β are both locally compact, then this is a homeomorphism, see Homeomorph.curry.

Instances For
@[simp]
theorem ContinuousMap.curry_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : C(α × β, γ)) (a : α) (b : β) :
↑(↑() a) b = f (a, b)
theorem ContinuousMap.continuous_curry {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [LocallyCompactSpace (α × β)] :
Continuous ContinuousMap.curry

The currying process is a continuous map between function spaces.

theorem ContinuousMap.continuous_uncurry_of_continuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : C(α, C(β, γ))) :
Continuous (Function.uncurry fun x y => ↑(f x) y)

The uncurried form of a continuous map α → C(β, γ) is a continuous map α × β → γ.

@[simp]
theorem ContinuousMap.uncurry_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : C(α, C(β, γ))) :
∀ (a : α × β), ↑() a = Function.uncurry (fun x y => ↑(f x) y) a
def ContinuousMap.uncurry {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : C(α, C(β, γ))) :
C(α × β, γ)

The uncurried form of a continuous map α → C(β, γ) as a continuous map α × β → γ (if β is locally compact). If α is also locally compact, then this is a homeomorphism between the two function spaces, see Homeomorph.curry.

Instances For
theorem ContinuousMap.continuous_uncurry {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] :
Continuous ContinuousMap.uncurry

The uncurrying process is a continuous map between function spaces.

def ContinuousMap.const' {α : Type u_1} {β : Type u_2} [] [] :
C(β, C(α, β))

The family of constant maps: β → C(α, β) as a continuous map.

Instances For
@[simp]
theorem ContinuousMap.coe_const' {α : Type u_1} {β : Type u_2} [] [] :
ContinuousMap.const' =
theorem ContinuousMap.continuous_const' {α : Type u_1} {β : Type u_2} [] [] :
def Homeomorph.curry {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] :
C(α × β, γ) ≃ₜ C(α, C(β, γ))

Currying as a homeomorphism between the function spaces C(α × β, γ) and C(α, C(β, γ)).

Instances For
def Homeomorph.continuousMapOfUnique {α : Type u_1} {β : Type u_2} [] [] [] :
β ≃ₜ C(α, β)

If α has a single element, then β is homeomorphic to C(α, β).

Instances For
@[simp]
theorem Homeomorph.continuousMapOfUnique_apply {α : Type u_1} {β : Type u_2} [] [] [] (b : β) (a : α) :
↑(Homeomorph.continuousMapOfUnique b) a = b
@[simp]
theorem Homeomorph.continuousMapOfUnique_symm_apply {α : Type u_1} {β : Type u_2} [] [] [] (f : C(α, β)) :
↑(Homeomorph.symm Homeomorph.continuousMapOfUnique) f = f default
theorem QuotientMap.continuous_lift_prod_left {X₀ : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [] [] [] [] {f : X₀X} (hf : ) {g : X × YZ} (hg : Continuous fun p => g (f p.fst, p.snd)) :
theorem QuotientMap.continuous_lift_prod_right {X₀ : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [] [] [] [] {f : X₀X} (hf : ) {g : Y × XZ} (hg : Continuous fun p => g (p.fst, f p.snd)) :