English
The compact-open topology on the space of continuous maps C(X, Y) is generated from subbasic sets {f : maps to} with respect to compact K and open U, i.e., {f | MapsTo f K U}.
Русский
Компактно-открытая топология на пространстве непрерывных отображений C(X,Y) порождается подбазой, состоящей из множеств {f | MapsTo f K U} для компактного K и открытого U.
LaTeX
$$$ \\text{compactOpen} \\;\\text{space} = \\mathrm{generateFrom} (\\mathrm{image2} (\\lambda K U, \\{ f : C(X,Y) \\mid \\mathrm{MapsTo} f K U\\}) \n {K | IsCompact K} {U | IsOpen U}) $$$
Lean4
/-- The compact-open topology on the space of continuous maps `C(X, Y)`. -/
instance compactOpen : TopologicalSpace C(X, Y) :=
.generateFrom <| image2 (fun K U ↦ {f | MapsTo f K U}) {K | IsCompact K} {U | IsOpen U}
