# 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

A generating set for the compact-open topology (when `s`

is compact and `u`

is open).

## Instances For

Definition of `ContinuousMap.compactOpen`

in terms of `Set.image2`

.

C(α, -) is a functor.

If `g : C(β, γ)`

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

is a topology inducing map too.

If `g : C(β, γ)`

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

is an embedding too.

C(-, γ) is a functor.

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*.

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

is continuous if `α`

is locally compact.

See also `ContinuousMap.continuous_eval`

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.

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.

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 `α`

.

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.

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 `α`

.

The coevaluation map `β → C(α, β × α)`

sending a point `x : β`

to the continuous function
on `α`

sending `y`

to `(x, y)`

.

## Instances For

Auxiliary definition, see `ContinuousMap.curry`

and `Homeomorph.curry`

.

## Instances For

If a map `α × β → γ`

is continuous, then its curried form `α → C(β, γ)`

is continuous.

To show continuity of a map `α → C(β, γ)`

, it suffices to show that its uncurried form
`α × β → γ`

is continuous.

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

The currying process is a continuous map between function spaces.

The uncurried form of a continuous map `α → C(β, γ)`

is a continuous map `α × β → γ`

.

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

The uncurrying process is a continuous map between function spaces.

The family of constant maps: `β → C(α, β)`

as a continuous map.

## Instances For

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

and `C(α, C(β, γ))`

.

## Instances For

If `α`

has a single element, then `β`

is homeomorphic to `C(α, β)`

.