Second-countability of pseudometrizable Lindelöf spaces

Factored out from Mathlib/Topology/Compactness/Lindelof.lean to avoid circular dependencies.

instance SecondCountableTopology.ofPseudoMetrizableSpaceLindelofSpace {X : Type u_1} [TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] [LindelofSpace X] : SecondCountableTopology X