Second countability of the reals

We prove that EReal, ℝ≥0 and ℝ≥0∞ are second countable. In the process, we also provide the instance ProperSpace ℝ≥0.

instance EReal.instSecondCountableTopology : SecondCountableTopology EReal

Instances for ℝ≥0 are inherited from the corresponding structures on the reals.

instance NNReal.instSecondCountableTopology : SecondCountableTopology NNReal

instance NNReal.instProperSpace : ProperSpace NNReal

instance ENNReal.instSecondCountableTopology : SecondCountableTopology ENNReal