Topological structure on EReal

We endow EReal with the order topology.

Implementation

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 EReal.instSecondCountableTopology : SecondCountableTopology EReal

Negation

instance EReal.instContinuousNeg : ContinuousNeg EReal