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)

instance instIsOrderBornology : IsOrderBornology ℝ

Topological structure on EReal

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

instance EReal.instTopologicalSpace : TopologicalSpace EReal

Equations

• EReal.instTopologicalSpace = Preorder.topology EReal

instance EReal.instOrderTopology : OrderTopology EReal

instance EReal.instT5Space : T5Space EReal

instance EReal.instT2Space : T2Space EReal

theorem EReal.denseRange_ratCast : DenseRange fun (r : ℚ) => ↑↑r

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

instance ENNReal.instOrderTopology : OrderTopology ENNReal

instance ENNReal.instT2Space : T2Space ENNReal

instance ENNReal.instT5Space : T5Space ENNReal

instance ENNReal.instT4Space : T4Space ENNReal

Instances for the following typeclasses are defined:

• OrderTopology ℝ≥0
• IsOrderBornology ℝ≥0

Everything is inherited from the corresponding structures on the reals.

instance NNReal.instOrderTopology : OrderTopology NNReal

instance NNReal.instIsOrderBornology : IsOrderBornology NNReal