Second countability of the reals

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

instance instProperSpaceReal : ProperSpace ℝ

instance instSecondCountableTopologyReal : SecondCountableTopology ℝ

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