Theorems · Theorem · general topology

ContinuousMap.compactOpen_eq_iInf_induced

∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  ContinuousMap.compactOpen =
    ⨅ K, ⨅ (_ : 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.

Defined in

Mathlib.Topology.CompactOpen

Cited by

2 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpace