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] : TopologicalSpace.PseudoMetrizableSpace C(X, Y)

instance ContinuousMap.instMetrizableSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] [SigmaCompactSpace X] [TopologicalSpace Y] [TopologicalSpace.MetrizableSpace Y] : TopologicalSpace.MetrizableSpace C(X, Y)