Metrizability of C(X, Y) #
If X is a weakly locally compact σ-compact space and Y is a (pseudo)metrizable space,
then C(X, Y) is a (pseudo)metrizable space.
instance
ContinuousMap.instPseudoMetrizableSpace
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[WeaklyLocallyCompactSpace X]
[SigmaCompactSpace X]
[TopologicalSpace Y]
[TopologicalSpace.PseudoMetrizableSpace Y]
:
instance
ContinuousMap.instMetrizableSpace
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[WeaklyLocallyCompactSpace X]
[SigmaCompactSpace X]
[TopologicalSpace Y]
[TopologicalSpace.MetrizableSpace Y]
: