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

• ContinuousMap.compactOpen is the compact-open topology on C(X, Y). It is declared as an instance.
• ContinuousMap.coev is the coevaluation map Y → C(X, Y × X). It is always continuous.
• ContinuousMap.curry is the currying map C(X × Y, Z) → C(X, C(Y, Z)). This map always exists and it is continuous as long as X × Y is locally compact.
• ContinuousMap.uncurry is the uncurrying map C(X, C(Y, Z)) → C(X × Y, Z). For this map to exist, we need Y to be locally compact. If X is also locally compact, then this map is continuous.
• Homeomorph.curry combines the currying and uncurrying operations into a homeomorphism C(X × Y, Z) ≃ₜ C(X, C(Y, Z)). This homeomorphism exists if X and Y are locally compact.
• ContinuousMap.prodHomeomorph and ContinuousMap.prodHomeomorph' are the homeomorphism C(X, Y × Z) ≃ₜ C(X, Y) × C(X, Z), f ↦ (fst ∘ f, snd ∘ f). It exists if Y and Z are R₁ spaces, or if X is an R₁ space.

Tags

compact-open, curry, function space

@[instance_reducible]

instance ContinuousMap.compactOpen {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] : TopologicalSpace C(X, Y)

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] : 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_setOfPred_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}

@[deprecated ContinuousMap.isOpen_setOfPred_mapsTo (since := "2026-07-09")]

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}

Alias of ContinuousMap.isOpen_setOfPred_mapsTo.

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.isOpen_setOfPred_range_subset {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {U : Set Y} [CompactSpace X] (hU : IsOpen U) : IsOpen {f : C(X, Y) | Set.range ⇑f ⊆ U}

@[deprecated ContinuousMap.isOpen_setOfPred_range_subset (since := "2026-07-09")]

theorem ContinuousMap.isOpen_setOf_range_subset {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {U : Set Y} [CompactSpace X] (hU : IsOpen U) : IsOpen {f : C(X, Y) | Set.range ⇑f ⊆ U}

Alias of ContinuousMap.isOpen_setOfPred_range_subset.

theorem ContinuousMap.eventually_range_subset {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {U : Set Y} [CompactSpace X] {f : C(X, Y)} (hU : IsOpen U) (h : Set.range ⇑f ⊆ U) : ∀ᶠ (g : C(X, Y)) in nhds f, Set.range ⇑g ⊆ 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 U → Set.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 : X → C(Y, Z)} : Continuous f ↔ ∀ (K : Set Y), IsCompact K → ∀ (U : Set Z), IsOpen U → IsOpen {x : X | Set.MapsTo (⇑(f x)) K U}

theorem ContinuousMap.hasBasis_nhds {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : (nhds f).HasBasis (fun (S : Set (Set X × Set Y)) => S.Finite ∧ ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K ∧ IsOpen U ∧ Set.MapsTo (⇑f) K U) fun (x : Set (Set X × Set Y)) => ⋂ KU ∈ x, {g : C(X, Y) | Set.MapsTo (⇑g) KU.1 KU.2}

theorem ContinuousMap.mem_nhds_iff {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {s : Set C(X, Y)} : s ∈ nhds f ↔ ∃ (S : Set (Set X × Set Y)), S.Finite ∧ (∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K ∧ IsOpen U ∧ Set.MapsTo (⇑f) K U) ∧ {g : C(X, Y) | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → Set.MapsTo (⇑g) K U} ⊆ s

theorem Filter.HasBasis.nhds_continuousMapConst {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {ι : Type u_6} {c : Y} {p : ι → Prop} {U : ι → Set Y} (h : (nhds c).HasBasis p U) : (nhds (ContinuousMap.const X c)).HasBasis (fun (Ki : Set X × ι) => IsCompact Ki.1 ∧ p Ki.2) fun (Ki : Set X × ι) => {f : C(X, Y) | Set.MapsTo (⇑f) Ki.1 (U Ki.2)}

theorem ContinuousMap.continuous_postcomp {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (g : C(Y, Z)) : Continuous g.comp

C(X, ·) is a functor.

theorem ContinuousMap.postcomp_injective {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (g : C(Y, Z)) (hg : Function.Injective ⇑g) : Function.Injective g.comp

If g : C(Y, Z) is injective, then the composition ContinuousMap.comp g : C(X, Y) → C(X, Z) is injective too.

theorem ContinuousMap.isInducing_postcomp {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (g : C(Y, Z)) (hg : Topology.IsInducing ⇑g) : Topology.IsInducing g.comp

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.isEmbedding_postcomp {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (g : C(Y, Z)) (hg : Topology.IsEmbedding ⇑g) : Topology.IsEmbedding g.comp

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_precomp {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)) => g.comp f

C(·, Z) is a functor.

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

Precomposition by a continuous map is itself a continuous map between spaces of continuous maps.

Equations

• ContinuousMap.compRightContinuousMap Z f = { toFun := fun (g : C(Y, Z)) => g.comp f, continuous_toFun := ⋯ }

@[simp]

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

def Homeomorph.arrowCongr {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {T : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace T] (φ : X ≃ₜ Z) (ψ : Y ≃ₜ T) : C(X, Y) ≃ₜ C(Z, T)

Any pair of homeomorphisms X ≃ₜ Z and Y ≃ₜ T gives rise to a homeomorphism C(X, Y) ≃ₜ C(Z, T).

Equations

• One or more equations did not get rendered due to their size.

theorem ContinuousMap.continuous_prodMk_const {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] : Continuous fun (p : X × C(Y, Z)) => (const Y p.1).prodMk p.2

The map from X × C(Y, Z) to C(Y, X × Z) is continuous.

theorem ContinuousMap.continuous_prodMk_of_locallyCompactPair {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h : ∀ (K : Set X), IsCompact K → LocallyCompactPair (↑K) (Y × Z)) : Continuous fun (p : C(X, Y) × C(X, Z)) => p.1.prodMk p.2

The pairing map C(X, Y) × C(X, Z) → C(X, Y × Z), (f, g) ↦ f.prodMk g, is continuous for the compact-open topologies, provided that (K, Y × Z) is a locally compact pair for every compact set K ⊆ X.

theorem ContinuousMap.continuous_prodMk {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [R1Space Y] [R1Space Z] : Continuous fun (p : C(X, Y) × C(X, Z)) => p.1.prodMk p.2

The pairing map C(X, Y) × C(X, Z) → C(X, Y × Z), (f, g) ↦ f.prodMk g, is continuous for the compact-open topologies, provided that Y and Z are R₁ spaces.

theorem ContinuousMap.continuous_prodMk' {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [R1Space X] : Continuous fun (p : C(X, Y) × C(X, Z)) => p.1.prodMk p.2

The pairing map C(X, Y) × C(X, Z) → C(X, Y × Z), (f, g) ↦ f.prodMk g, is continuous for the compact-open topologies, provided that X is an R₁ space.

def ContinuousMap.prodHomeomorph (X : Type u_2) (Y : Type u_3) (Z : Type u_4) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [R1Space Y] [R1Space Z] : C(X, Y × Z) ≃ₜ C(X, Y) × C(X, Z)

The homeomorphism C(X, Y × Z) ≃ₜ C(X, Y) × C(X, Z), f ↦ (fst ∘ f, snd ∘ f), with inverse (f, g) ↦ f.prodMk g, for the compact-open topologies, when Y and Z are R₁ spaces. See ContinuousMap.prodHomeomorph' for the version with a hypothesis on X instead.

Equations

• ContinuousMap.prodHomeomorph X Y Z = { toEquiv := ContinuousMap.prodEquiv X Y Z, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousMap.prodHomeomorph_apply (X : Type u_2) (Y : Type u_3) (Z : Type u_4) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [R1Space Y] [R1Space Z] (f : C(X, Y × Z)) : (prodHomeomorph X Y Z) f = (fst.comp f, snd.comp f)

@[simp]

theorem ContinuousMap.prodHomeomorph_symm_apply (X : Type u_2) (Y : Type u_3) (Z : Type u_4) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [R1Space Y] [R1Space Z] (p : C(X, Y) × C(X, Z)) : (prodHomeomorph X Y Z).symm p = p.1.prodMk p.2

def ContinuousMap.prodHomeomorph' (X : Type u_2) (Y : Type u_3) (Z : Type u_4) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [R1Space X] : C(X, Y × Z) ≃ₜ C(X, Y) × C(X, Z)

The homeomorphism C(X, Y × Z) ≃ₜ C(X, Y) × C(X, Z), f ↦ (fst ∘ f, snd ∘ f), with inverse (f, g) ↦ f.prodMk g, for the compact-open topologies, when X is an R₁ space. See ContinuousMap.prodHomeomorph for the version with hypotheses on Y and Z instead.

Equations

• ContinuousMap.prodHomeomorph' X Y Z = { toEquiv := ContinuousMap.prodEquiv X Y Z, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousMap.prodHomeomorph'_symm_apply (X : Type u_2) (Y : Type u_3) (Z : Type u_4) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [R1Space X] (p : C(X, Y) × C(X, Z)) : (prodHomeomorph' X Y Z).symm p = p.1.prodMk p.2

@[simp]

theorem ContinuousMap.prodHomeomorph'_apply (X : Type u_2) (Y : Type u_3) (Z : Type u_4) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [R1Space X] (f : C(X, Y × Z)) : (prodHomeomorph' X Y Z) f = (fst.comp f, snd.comp f)

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] : Continuous fun (x : C(X, Y) × C(Y, Z)) => x.2.comp x.1

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_6} {l : Filter α} {g : α → C(Y, Z)} {g₀ : C(Y, Z)} {f : α → C(X, Y)} {f₀ : C(X, Y)} (hg : Tendsto g l (nhds g₀)) (hf : Tendsto f l (nhds f₀)) : Tendsto (fun (a : α) => (g a).comp (f a)) l (nhds (g₀.comp 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_6} [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') => (g x).comp (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_6} [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') => (g x).comp (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_6} [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') => (g x).comp (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_6} [TopologicalSpace X'] {g : X' → C(Y, Z)} {f : X' → C(X, Y)} (hg : Continuous g) (hf : Continuous f) : Continuous fun (x : X') => (g x).comp (f x)

instance ContinuousMap.instContinuousEvalOfLocallyCompactPair {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [LocallyCompactPair X Y] : ContinuousEval C(X, Y) X Y

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

instance ContinuousMap.instContinuousEvalConst {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] : ContinuousEvalConst C(X, Y) X Y

theorem ContinuousMap.isClosed_setOfPred_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}

@[deprecated ContinuousMap.isClosed_setOfPred_mapsTo (since := "2026-07-09")]

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}

Alias of ContinuousMap.isClosed_setOfPred_mapsTo.

theorem ContinuousMap.isClopen_setOfPred_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}

@[deprecated ContinuousMap.isClopen_setOfPred_mapsTo (since := "2026-07-09")]

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}

Alias of ContinuousMap.isClopen_setOfPred_mapsTo.

theorem ContinuousMap.specializes_coe {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} : ⇑f ⤳ ⇑g ↔ f ⤳ g

theorem ContinuousMap.inseparable_coe {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} : Inseparable ⇑f ⇑g ↔ Inseparable f g

instance ContinuousMap.instT0Space {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [T0Space Y] : T0Space C(X, Y)

instance ContinuousMap.instR0Space {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [R0Space Y] : R0Space C(X, Y)

instance ContinuousMap.instT1Space {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y] : T1Space C(X, Y)

instance ContinuousMap.instR1Space {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [R1Space Y] : R1Space C(X, Y)

instance ContinuousMap.instT2Space {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] : T2Space C(X, Y)

instance ContinuousMap.instRegularSpace {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [RegularSpace Y] : RegularSpace C(X, Y)

instance ContinuousMap.instT3Space {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [T3Space Y] : T3Space C(X, Y)

def ContinuousMap.homeoFnOfDiscrete {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [DiscreteTopology X] : C(X, Y) ≃ₜ (X → Y)

The continuous functions from X to Y are the same as the plain functions when X is discrete.

Equations

• ContinuousMap.homeoFnOfDiscrete = { toEquiv := ContinuousMap.equivFnOfDiscrete, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousMap.toEquiv_homeoFnOfDiscrete {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [DiscreteTopology X] : homeoFnOfDiscrete.toEquiv = equivFnOfDiscrete

theorem ContinuousMap.homeoFnOfDiscrete_symm_apply_apply {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [DiscreteTopology X] (f : X → Y) (a✝ : X) : (homeoFnOfDiscrete.symm f) a✝ = f a✝

theorem ContinuousMap.homeoFnOfDiscrete_apply {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [DiscreteTopology X] (f : C(X, Y)) (a : X) : homeoFnOfDiscrete f a = f a

@[simp]

theorem ContinuousMap.coe_homeoFnOfDiscrete {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [DiscreteTopology X] : ⇑homeoFnOfDiscrete = DFunLike.coe

@[simp]

theorem ContinuousMap.homeoFnOfDiscrete_symm_apply {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [DiscreteTopology X] (f : X → Y) : ⇑(homeoFnOfDiscrete.symm f) = f

theorem ContinuousMap.isHomeomorph_coe {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [DiscreteTopology X] : IsHomeomorph DFunLike.coe

theorem ContinuousMap.continuous_restrict {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (s : Set X) : Continuous fun (F : C(X, Y)) => restrict s F

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) : compactOpen ≤ TopologicalSpace.induced (restrict s) compactOpen

theorem ContinuousMap.compactOpen_eq_iInf_induced {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] : compactOpen = ⨅ (K : Set X), ⨅ (_ : IsCompact K), TopologicalSpace.induced (restrict K) 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.

theorem ContinuousMap.nhds_compactOpen_eq_iInf_nhds_induced {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : nhds f = ⨅ (s : Set X), ⨅ (_ : IsCompact s), Filter.comap (restrict s) (nhds (restrict s f))

theorem ContinuousMap.tendsto_compactOpen_restrict {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {ι : Type u_6} {l : Filter ι} {F : ι → C(X, Y)} {f : C(X, Y)} (hFf : Filter.Tendsto F l (nhds f)) (s : Set X) : Filter.Tendsto (fun (i : ι) => restrict s (F i)) l (nhds (restrict s f))

theorem ContinuousMap.tendsto_compactOpen_iff_forall {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {ι : Type u_6} {l : Filter ι} (F : ι → C(X, Y)) (f : C(X, Y)) : Filter.Tendsto F l (nhds f) ↔ ∀ (K : Set X), IsCompact K → Filter.Tendsto (fun (i : ι) => restrict K (F i)) l (nhds (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_6} {l : Filter ι} [l.NeBot] (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 : ι) => 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.

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

• ContinuousMap.coev X Y b = { toFun := Prod.mk b, continuous_toFun := ⋯ }

@[simp]

theorem ContinuousMap.coev_apply (X : Type u_2) (Y : Type u_3) [TopologicalSpace X] [TopologicalSpace Y] (b : Y) : ⇑(coev X Y b) = Prod.mk b

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

theorem ContinuousMap.continuous_coev {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] : Continuous (coev X Y)

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)) : C(X, C(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

• f.curry = { toFun := fun (a : X) => { toFun := Function.curry (⇑f) a, continuous_toFun := ⋯ }, continuous_toFun := ⋯ }

@[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) : (f.curry a) b = f (a, b)

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 : X → C(Y, Z)) (h : Continuous (Function.uncurry fun (x : X) (y : Y) => (f x) y)) : Continuous f

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

theorem ContinuousMap.continuousOn_of_continuousOn_uncurry {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {s : Set X} (f : X → C(Y, Z)) (h : ContinuousOn (Function.uncurry fun (x : X) (y : Y) => (f x) y) (s ×ˢ Set.univ)) : ContinuousOn f s

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

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

• f.uncurry = { toFun := Function.uncurry fun (x : X) (y : Y) => (f x) y, continuous_toFun := ⋯ }

@[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) : f.uncurry a✝ = Function.uncurry (fun (x : X) (y : Y) => (f x) y) a✝

theorem ContinuousMap.continuous_uncurry {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [LocallyCompactSpace X] [LocallyCompactSpace Y] : Continuous uncurry

The uncurrying process is a continuous map between function spaces.

def ContinuousMap.const' {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] : C(Y, C(X, Y))

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

Equations

• ContinuousMap.const' = ContinuousMap.fst.curry

@[simp]

theorem ContinuousMap.coe_const' {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] : ⇑const' = const X

theorem ContinuousMap.continuous_const' {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] : Continuous (const X)

theorem ContinuousMap.continuous_mkD_of_uncurry {X : Type u_2} {Y : Type u_3} {T : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace T] (f : T → X → Y) (g : C(X, Y)) (f_cont : Continuous (Function.uncurry f)) : Continuous fun (x : T) => mkD (f x) g

A variant of ContinuousMap.continuous_of_continuous_uncurry in terms of ContinuousMap.mkD. Of course, in this particular setting, fun x ↦ mkD (f x) g is just f, but the mkD spelling appears naturally in the context of C(α, β)-valued integration.

theorem ContinuousMap.continuousOn_mkD_of_uncurry {X : Type u_2} {Y : Type u_3} {T : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace T] {s : Set T} (f : T → X → Y) (g : C(X, Y)) (f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ Set.univ)) : ContinuousOn (fun (x : T) => mkD (f x) g) s

theorem ContinuousMap.continuous_mkD_restrict_of_uncurry {X : Type u_2} {Y : Type u_3} {T : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace T] {t : Set X} (f : T → X → Y) (g : C(↑t, Y)) (f_cont : ContinuousOn (Function.uncurry f) (Set.univ ×ˢ t)) : Continuous fun (x : T) => mkD (t.domRestrict (f x)) g

theorem ContinuousMap.continuousOn_mkD_restrict_of_uncurry {X : Type u_2} {Y : Type u_3} {T : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace T] {s : Set T} {t : Set X} (f : T → X → Y) (g : C(↑t, Y)) (f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)) : ContinuousOn (fun (x : T) => mkD (t.domRestrict (f x)) g) s

def Homeomorph.curry {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [LocallyCompactSpace X] [LocallyCompactSpace Y] : C(X × Y, Z) ≃ₜ C(X, C(Y, Z))

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

Equations

• Homeomorph.curry = { toFun := ContinuousMap.curry, invFun := ContinuousMap.uncurry, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def Homeomorph.continuousMapOfUnique {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [Unique X] : Y ≃ₜ C(X, Y)

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

Equations

• Homeomorph.continuousMapOfUnique = { toFun := ContinuousMap.const X, invFun := fun (f : C(X, Y)) => f default, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.continuousMapOfUnique_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [Unique X] (y : Y) (x : X) : (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)) : continuousMapOfUnique.symm f = f default

theorem Topology.IsQuotientMap.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 : IsQuotientMap f) {g : X × Y → Z} (hg : Continuous fun (p : X₀ × Y) => g (f p.1, p.2)) : Continuous g

theorem Topology.IsQuotientMap.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 : IsQuotientMap f) {g : Y × X → Z} (hg : Continuous fun (p : Y × X₀) => g (p.1, f p.2)) : Continuous g