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