Topology on extended non-negative reals

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

instance ENNReal.instSecondCountableTopology : SecondCountableTopology ENNReal

instance ENNReal.instMetrizableSpace : TopologicalSpace.MetrizableSpace ENNReal

theorem ENNReal.isEmbedding_coe : Topology.IsEmbedding ENNReal.ofNNReal

theorem ENNReal.tendsto_coe {α : Type u_1} {f : Filter α} {m : α → NNReal} {a : NNReal} : Filter.Tendsto (fun (a : α) => ↑(m a)) f (nhds ↑a) ↔ Filter.Tendsto m f (nhds a)

theorem ENNReal.isOpenEmbedding_coe : Topology.IsOpenEmbedding ENNReal.ofNNReal

theorem ENNReal.nhds_coe_coe {r p : NNReal} : nhds (↑r, ↑p) = Filter.map (fun (p : NNReal × NNReal) => (↑p.1, ↑p.2)) (nhds (r, p))

instance ENNReal.instContinuousAdd : ContinuousAdd ENNReal

instance ENNReal.instContinuousInv : ContinuousInv ENNReal