# mathlibdocumentation

topology.compact_open

# 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 #

• compact_open is the compact-open topology on C(α, β). It is declared as an instance.
• ev is the evaluation map C(α, β) × α → β. It is continuous as long as α is locally compact.
• coev is the coevaluation map β → C(α, β × α). It is always continuous.
• continuous_map.curry is the currying map C(α × β, γ) → C(α, C(β, γ)). This map always exists and it is continuous as long as α × β is locally compact.
• continuous_map.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 continuous_map.compact_open.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).

Equations
@[instance]
def continuous_map.compact_open {α : Type u_1} {β : Type u_2}  :
Equations
theorem continuous_map.continuous_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : C(β, γ)) :

C(α, -) is a functor.

def continuous_map.ev (α : Type u_1) (β : Type u_2) (p : C(α, β) × α) :
β

The evaluation map map C(α, β) × α → β

Equations
theorem continuous_map.continuous_ev {α : Type u_1} {β : Type u_2}  :

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

theorem continuous_map.continuous_ev₁ {α : Type u_1} {β : Type u_2} (a : α) :
continuous (λ (f : C(α, β)), f a)
@[instance]
def continuous_map.t2_space {α : Type u_1} {β : Type u_2} [t2_space β]  :
theorem continuous_map.compact_open_le_induced {α : Type u_1} {β : Type u_2} (s : set α) :
theorem continuous_map.compact_open_eq_Inf_induced {α : Type u_1} {β : Type u_2}  :

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 continuous_map.continuous_restrict {α : Type u_1} {β : Type u_2} (s : set α) :
continuous (λ (F : C(α, β)),

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 continuous_map.nhds_compact_open_eq_Inf_nhds_induced {α : Type u_1} {β : Type u_2} (f : C(α, β)) :
𝓝 f = ⨅ (s : set α) (hs : ,
theorem continuous_map.tendsto_compact_open_restrict {α : Type u_1} {β : Type u_2} {ι : Type u_3} {l : filter ι} {F : ι → C(α, β)} {f : C(α, β)} (hFf : (𝓝 f)) (s : set α) :
filter.tendsto (λ (i : ι), (F i)) l (𝓝 f))
theorem continuous_map.tendsto_compact_open_iff_forall {α : Type u_1} {β : Type u_2} {ι : Type u_3} {l : filter ι} (F : ι → C(α, β)) (f : C(α, β)) :
(𝓝 f) ∀ (s : set α), filter.tendsto (λ (i : ι), (F i)) l (𝓝 f))
theorem continuous_map.exists_tendsto_compact_open_iff_forall {α : Type u_1} {β : Type u_2} [t2_space α] [t2_space β] {ι : Type u_3} {l : filter ι} [l.ne_bot] (F : ι → C(α, β)) :
(∃ (f : C(α, β)), (𝓝 f)) ∀ (s : set α), (∃ (f : C(s, β)), filter.tendsto (λ (i : ι), (F i)) l (𝓝 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 continuous_map.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).

Equations
theorem continuous_map.image_coev {α : Type u_1} {β : Type u_2} {y : β} (s : set α) :
y) '' s = {y}.prod s
theorem continuous_map.continuous_coev {α : Type u_1} {β : Type u_2}  :
def continuous_map.curry' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : C(α × β, γ)) (a : α) :
C(β, γ)

Auxiliary definition, see continuous_map.curry and homeomorph.curry.

Equations
theorem continuous_map.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 continuous_map.continuous_of_continuous_uncurry {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → C(β, γ)) (h : continuous (function.uncurry (λ (x : α) (y : β), (f x) y))) :

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

def continuous_map.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.

Equations
theorem continuous_map.continuous_curry {α : Type u_1} {β : Type u_2} {γ : Type u_3} [locally_compact_space × β)] :

The currying process is a continuous map between function spaces.

@[simp]
theorem continuous_map.curry_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : C(α × β, γ)) (a : α) (b : β) :
((f.curry) a) b = f (a, b)
theorem continuous_map.continuous_uncurry_of_continuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : C(α, C(β, γ))) :
continuous (function.uncurry (λ (x : α) (y : β), (f x) y))

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

def continuous_map.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.

Equations
theorem continuous_map.continuous_uncurry {α : Type u_1} {β : Type u_2} {γ : Type u_3}  :

The uncurrying process is a continuous map between function spaces.

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

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

Equations
@[simp]
theorem continuous_map.coe_const' {α : Type u_1} {β : Type u_2}  :
theorem continuous_map.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(β, γ)).

Equations
def homeomorph.continuous_map_of_unique {α : Type u_1} {β : Type u_2} [unique α] :
β ≃ₜ C(α, β)

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

Equations
@[simp]
theorem homeomorph.continuous_map_of_unique_apply {α : Type u_1} {β : Type u_2} [unique α] (b : β) (a : α) :
@[simp]
theorem homeomorph.continuous_map_of_unique_symm_apply {α : Type u_1} {β : Type u_2} [unique α] (f : C(α, β)) :