English
The topology on the path space Path x y is the induced topology from the compact-open topology on C(I,X).
Русский
Топология пространства путей Path x y задаётся индуцированной топологией от компактно-открытой топологии на C(I,X).
LaTeX
$$$\\text{TopologicalSpace}(Path(x,y)) = \\mathrm{TopologicalSpace}.induced((\\uparrow) : Path(x,y) \\to C(I,X))\\;\\text{compactOpen}$$$
Lean4
/-- The following instance defines the topology on the path space to be induced from the
compact-open topology on the space `C(I,X)` of continuous maps from `I` to `X`.
-/
instance instTopologicalSpace : TopologicalSpace (Path x y) :=
TopologicalSpace.induced ((↑) : _ → C(I, X)) ContinuousMap.compactOpen
