Metrizable separability and the Lindelöf property (source code)

= Metrizable separability and the Lindelöf property

A <metrizable space> is <separable> exactly when it is <Lindelöf>. A <countable> <dense subset> gives a <countable> <topological basis> of balls with rational radii, hence the open-cover property. Conversely, choose <countable> subcovers of all radius-$1/n$ ball covers; their centers form a <countable> <dense subset>.