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]
:
Equations
- ⋯ = ⋯