English
The compact-open topology on C(X,Y) equals the infimum (greatest lower bound) of the induced topologies from restricting to all compact subsets K of X.
Русский
Компактно-открытая топология равна наибольшему нижнему предку инфинумы Induced( Restrict_K ) по всем компактным подмножествам K ⊆ X.
LaTeX
$$$\text{compactOpen} = \bigwedge_{K\subseteq X,\ IsCompact(K)} \; .\text{induced} (\text{restrict}_K)\ \text{compactOpen}$$$
Lean4
/-- 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 compactOpen_eq_iInf_induced :
(ContinuousMap.compactOpen : TopologicalSpace C(X, Y)) =
⨅ (K : Set X) (_ : IsCompact K), .induced (.restrict K) ContinuousMap.compactOpen :=
by
refine le_antisymm (le_iInf₂ fun s _ ↦ compactOpen_le_induced s) ?_
refine le_generateFrom <| forall_mem_image2.2 fun K (hK : IsCompact K) U hU ↦ ?_
refine TopologicalSpace.le_def.1 (iInf₂_le K hK) _ ?_
convert isOpen_induced (isOpen_setOf_mapsTo (isCompact_iff_isCompact_univ.1 hK) hU)
simp [Subtype.forall, MapsTo]
