# The reals are equipped with their order topology #

This file contains results related to the order topology on (extended) (non-negative) real numbers. We

- prove that `ℝ` and `ℝ≥0` are equipped with the order topology and bornology,
- endow `EReal` with the order topology (and prove some very basic lemmas),
- define the topology `ℝ≥0∞` (which is the order topology, not the `EMetricSpace` topology)

### Topological structure on `EReal` #

We endow `EReal` with the order topology. Most proofs are adapted from the corresponding proofs on `ℝ≥0∞`.

source
instance EReal.instTopologicalSpace :
TopologicalSpace EReal
Equations

- EReal.instTopologicalSpace = Preorder.topology EReal

source
instance EReal.instOrderTopology :
OrderTopology EReal
source
instance EReal.instT5Space :
T5Space EReal
source
instance EReal.instT2Space :
T2Space EReal
source
theorem EReal.denseRange_ratCast :
DenseRange fun (r : ℚ) => ↑↑r
source
instance ENNReal.instTopologicalSpace :
TopologicalSpace ENNReal

Topology on `ℝ≥0∞`.

Note: this is different from the `EMetricSpace` topology. The `EMetricSpace` topology has `IsOpen {∞}`, while this topology doesn't have singleton elements.

Equations

- ENNReal.instTopologicalSpace = Preorder.topology ENNReal

source
instance ENNReal.instOrderTopology :
OrderTopology ENNReal
source
instance ENNReal.instT2Space :
T2Space ENNReal
source
instance ENNReal.instT5Space :
T5Space ENNReal
source
instance ENNReal.instT4Space :
T4Space ENNReal