Second-countability of pseudometrizable Lindelöf spaces

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

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