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 #

Tags #

compact-open, curry, function space

The compact-open topology on the space of continuous maps C(X, Y).

Equations
  • One or more equations did not get rendered due to their size.
theorem ContinuousMap.compactOpen_eq {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] :
ContinuousMap.compactOpen = TopologicalSpace.generateFrom (Set.image2 (fun (K : Set X) (U : Set Y) => {f : C(X, Y) | Set.MapsTo (f) K U}) {K : Set X | IsCompact K} {t : Set Y | IsOpen t})

Definition of ContinuousMap.compactOpen.

theorem ContinuousMap.isOpen_setOf_mapsTo {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {K : Set X} {U : Set Y} (hK : IsCompact K) (hU : IsOpen U) :
IsOpen {f : C(X, Y) | Set.MapsTo (f) K U}
theorem ContinuousMap.eventually_mapsTo {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {K : Set X} {U : Set Y} {f : C(X, Y)} (hK : IsCompact K) (hU : IsOpen U) (h : Set.MapsTo (f) K U) :
∀ᶠ (g : C(X, Y)) in nhds f, Set.MapsTo (g) K U
theorem ContinuousMap.nhds_compactOpen {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) :
nhds f = ⨅ (K : Set X), ⨅ (_ : IsCompact K), ⨅ (U : Set Y), ⨅ (_ : IsOpen U), ⨅ (_ : Set.MapsTo (f) K U), Filter.principal {g : C(X, Y) | Set.MapsTo (g) K U}
theorem ContinuousMap.tendsto_nhds_compactOpen {α : Type u_1} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace Y] [TopologicalSpace Z] {l : Filter α} {f : αC(Y, Z)} {g : C(Y, Z)} :
Filter.Tendsto f l (nhds g) ∀ (K : Set Y), IsCompact K∀ (U : Set Z), IsOpen USet.MapsTo (g) K U∀ᶠ (a : α) in l, Set.MapsTo ((f a)) K U
theorem ContinuousMap.continuous_compactOpen {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XC(Y, Z)} :
Continuous f ∀ (K : Set Y), IsCompact K∀ (U : Set Z), IsOpen UIsOpen {x : X | Set.MapsTo ((f x)) K U}

C(X, ·) is a functor.

theorem ContinuousMap.inducing_comp {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (g : C(Y, Z)) (hg : Inducing g) :

If g : C(Y, Z) is a topology inducing map, then the composition ContinuousMap.comp g : C(X, Y) → C(X, Z) is a topology inducing map too.

theorem ContinuousMap.embedding_comp {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (g : C(Y, Z)) (hg : Embedding g) :

If g : C(Y, Z) is a topological embedding, then the composition ContinuousMap.comp g : C(X, Y) → C(X, Z) is an embedding too.

theorem ContinuousMap.continuous_comp_left {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : C(X, Y)) :
Continuous fun (g : C(Y, Z)) => ContinuousMap.comp g f

C(·, Z) is a functor.

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

theorem Filter.Tendsto.compCM {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [LocallyCompactPair Y Z] {α : Type u_5} {l : Filter α} {g : αC(Y, Z)} {g₀ : C(Y, Z)} {f : αC(X, Y)} {f₀ : C(X, Y)} (hg : Filter.Tendsto g l (nhds g₀)) (hf : Filter.Tendsto f l (nhds f₀)) :
Filter.Tendsto (fun (a : α) => ContinuousMap.comp (g a) (f a)) l (nhds (ContinuousMap.comp g₀ f₀))
theorem ContinuousAt.compCM {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [LocallyCompactPair Y Z] {X' : Type u_5} [TopologicalSpace X'] {a : X'} {g : X'C(Y, Z)} {f : X'C(X, Y)} (hg : ContinuousAt g a) (hf : ContinuousAt f a) :
ContinuousAt (fun (x : X') => ContinuousMap.comp (g x) (f x)) a
theorem ContinuousWithinAt.compCM {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [LocallyCompactPair Y Z] {X' : Type u_5} [TopologicalSpace X'] {a : X'} {g : X'C(Y, Z)} {f : X'C(X, Y)} {s : Set X'} (hg : ContinuousWithinAt g s a) (hf : ContinuousWithinAt f s a) :
ContinuousWithinAt (fun (x : X') => ContinuousMap.comp (g x) (f x)) s a
theorem ContinuousOn.compCM {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [LocallyCompactPair Y Z] {X' : Type u_5} [TopologicalSpace X'] {g : X'C(Y, Z)} {f : X'C(X, Y)} {s : Set X'} (hg : ContinuousOn g s) (hf : ContinuousOn f s) :
ContinuousOn (fun (x : X') => ContinuousMap.comp (g x) (f x)) s
theorem Continuous.compCM {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [LocallyCompactPair Y Z] {X' : Type u_5} [TopologicalSpace X'] {g : X'C(Y, Z)} {f : X'C(X, Y)} (hg : Continuous g) (hf : Continuous f) :
Continuous fun (x : X') => ContinuousMap.comp (g x) (f x)
@[deprecated Continuous.compCM]
theorem ContinuousMap.continuous.comp' {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [LocallyCompactPair Y Z] {X' : Type u_5} [TopologicalSpace X'] {g : X'C(Y, Z)} {f : X'C(X, Y)} (hf : Continuous f) (hg : Continuous g) :
Continuous fun (x : X') => ContinuousMap.comp (g x) (f x)
theorem ContinuousMap.continuous_eval {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [LocallyCompactPair X Y] :
Continuous fun (p : C(X, Y) × X) => p.1 p.2

The evaluation map C(X, Y) × X → Y is continuous if X, Y is a locally compact pair of spaces.

@[deprecated ContinuousMap.continuous_eval]
theorem ContinuousMap.continuous_eval' {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [LocallyCompactPair X Y] :
Continuous fun (p : C(X, Y) × X) => p.1 p.2

Alias of ContinuousMap.continuous_eval.


The evaluation map C(X, Y) × X → Y is continuous if X, Y is a locally compact pair of spaces.

theorem ContinuousMap.continuous_eval_const {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (a : X) :
Continuous fun (f : C(X, Y)) => f a

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

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

theorem ContinuousMap.continuous_coe {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] :
Continuous DFunLike.coe

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

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

theorem ContinuousMap.isClosed_setOf_mapsTo {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {t : Set Y} (ht : IsClosed t) (s : Set X) :
IsClosed {f : C(X, Y) | Set.MapsTo (f) s t}
theorem ContinuousMap.isClopen_setOf_mapsTo {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {K : Set X} {U : Set Y} (hK : IsCompact K) (hU : IsClopen U) :
IsClopen {f : C(X, Y) | Set.MapsTo (f) K U}

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

theorem ContinuousMap.compactOpen_le_induced {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (s : Set X) :
ContinuousMap.compactOpen TopologicalSpace.induced (ContinuousMap.restrict s) ContinuousMap.compactOpen
theorem ContinuousMap.compactOpen_eq_iInf_induced {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] :
ContinuousMap.compactOpen = ⨅ (K : Set X), ⨅ (_ : IsCompact K), TopologicalSpace.induced (ContinuousMap.restrict K) ContinuousMap.compactOpen

The compact-open topology on C(X, Y) is equal to the infimum of the compact-open topologies on C(s, Y) for s a compact subset of X. The key point of the proof is that for every compact set K, the universal set Set.univ : Set K is a compact set as well.

@[deprecated ContinuousMap.compactOpen_eq_iInf_induced]
theorem ContinuousMap.compactOpen_eq_sInf_induced {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] :
ContinuousMap.compactOpen = ⨅ (K : Set X), ⨅ (_ : IsCompact K), TopologicalSpace.induced (ContinuousMap.restrict K) ContinuousMap.compactOpen

Alias of ContinuousMap.compactOpen_eq_iInf_induced.


The compact-open topology on C(X, Y) is equal to the infimum of the compact-open topologies on C(s, Y) for s a compact subset of X. The key point of the proof is that for every compact set K, the universal set Set.univ : Set K is a compact set as well.

@[deprecated ContinuousMap.nhds_compactOpen_eq_iInf_nhds_induced]

Alias of ContinuousMap.nhds_compactOpen_eq_iInf_nhds_induced.

theorem ContinuousMap.tendsto_compactOpen_restrict {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {ι : Type u_5} {l : Filter ι} {F : ιC(X, Y)} {f : C(X, Y)} (hFf : Filter.Tendsto F l (nhds f)) (s : Set X) :
theorem ContinuousMap.tendsto_compactOpen_iff_forall {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {ι : Type u_5} {l : Filter ι} (F : ιC(X, Y)) (f : C(X, Y)) :
Filter.Tendsto F l (nhds f) ∀ (K : Set X), IsCompact KFilter.Tendsto (fun (i : ι) => ContinuousMap.restrict K (F i)) l (nhds (ContinuousMap.restrict K f))
theorem ContinuousMap.exists_tendsto_compactOpen_iff_forall {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [WeaklyLocallyCompactSpace X] [T2Space Y] {ι : Type u_5} {l : Filter ι} [Filter.NeBot l] (F : ιC(X, Y)) :
(∃ (f : C(X, Y)), Filter.Tendsto F l (nhds f)) ∀ (s : Set X), IsCompact s∃ (f : C(s, Y)), Filter.Tendsto (fun (i : ι) => ContinuousMap.restrict s (F i)) l (nhds f)

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

@[simp]
theorem ContinuousMap.coev_apply (X : Type u_2) (Y : Type u_3) [TopologicalSpace X] [TopologicalSpace Y] (b : Y) :
def ContinuousMap.coev (X : Type u_2) (Y : Type u_3) [TopologicalSpace X] [TopologicalSpace Y] (b : Y) :
C(X, Y × X)

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

Equations
Instances For
    theorem ContinuousMap.image_coev {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {y : Y} (s : Set X) :
    (ContinuousMap.coev X Y y) '' s = {y} ×ˢ s

    The coevaluation map Y → C(X, Y × X) is continuous (always).

    def ContinuousMap.curry {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : C(X × Y, Z)) :

    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
    Instances For
      @[simp]
      theorem ContinuousMap.curry_apply {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : C(X × Y, Z)) (a : X) (b : Y) :
      ((ContinuousMap.curry f) a) b = f (a, b)
      @[deprecated ContinuousMap.curry]
      def ContinuousMap.curry' {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : C(X × Y, Z)) (a : X) :
      C(Y, Z)

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

      Equations
      Instances For
        @[deprecated ContinuousMap.curry]

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

        theorem ContinuousMap.continuous_of_continuous_uncurry {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : XC(Y, Z)) (h : Continuous (Function.uncurry fun (x : X) (y : Y) => (f x) y)) :

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

        theorem ContinuousMap.continuous_curry {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [LocallyCompactSpace (X × Y)] :
        Continuous ContinuousMap.curry

        The currying process is a continuous map between function spaces.

        theorem ContinuousMap.continuous_uncurry_of_continuous {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [LocallyCompactSpace Y] (f : C(X, C(Y, Z))) :
        Continuous (Function.uncurry fun (x : X) (y : Y) => (f x) y)

        The uncurried form of a continuous map X → C(Y, Z) is a continuous map X × Y → Z.

        @[simp]
        theorem ContinuousMap.uncurry_apply {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [LocallyCompactSpace Y] (f : C(X, C(Y, Z))) :
        ∀ (a : X × Y), (ContinuousMap.uncurry f) a = Function.uncurry (fun (x : X) (y : Y) => (f x) y) a
        def ContinuousMap.uncurry {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [LocallyCompactSpace Y] (f : C(X, C(Y, Z))) :
        C(X × Y, Z)

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

        Equations
        Instances For

          The uncurrying process is a continuous map between function spaces.

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

          Equations
          Instances For
            @[simp]
            theorem ContinuousMap.coe_const' {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] :
            ContinuousMap.const' = ContinuousMap.const X

            Currying as a homeomorphism between the function spaces C(X × Y, Z) and C(X, C(Y, Z)).

            Equations
            • Homeomorph.curry = { toEquiv := { toFun := ContinuousMap.curry, invFun := ContinuousMap.uncurry, left_inv := , right_inv := }, continuous_toFun := , continuous_invFun := }
            Instances For

              If X has a single element, then Y is homeomorphic to C(X, Y).

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem Homeomorph.continuousMapOfUnique_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [Unique X] (y : Y) (x : X) :
                (Homeomorph.continuousMapOfUnique y) x = y
                @[simp]
                theorem Homeomorph.continuousMapOfUnique_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [Unique X] (f : C(X, Y)) :
                (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} [TopologicalSpace X₀] [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [LocallyCompactSpace Y] {f : X₀X} (hf : QuotientMap f) {g : X × YZ} (hg : Continuous fun (p : X₀ × Y) => g (f p.1, p.2)) :
                theorem QuotientMap.continuous_lift_prod_right {X₀ : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X₀] [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [LocallyCompactSpace Y] {f : X₀X} (hf : QuotientMap f) {g : Y × XZ} (hg : Continuous fun (p : Y × X₀) => g (p.1, f p.2)) :