Topological algebra properties of ℝ

This file defines topological field/(semi)ring structures on the (extended) (nonnegative) reals and shows the algebraic operations are (uniformly) continuous.

It also includes a bit of more general topological theory of the reals, needed to define the structures and prove continuity.

instance instNoncompactSpaceReal : NoncompactSpace ℝ

theorem Real.uniformContinuous_add : UniformContinuous fun (p : ℝ × ℝ) => p.1 + p.2

theorem Real.uniformContinuous_neg : UniformContinuous Neg.neg

instance instUniformAddGroupReal : UniformAddGroup ℝ

theorem Real.uniformContinuous_const_mul {x : ℝ} : UniformContinuous fun (x_1 : ℝ) => x * x_1

instance instIsTopologicalAddGroupReal : IsTopologicalAddGroup ℝ

instance instIsTopologicalRingReal : IsTopologicalRing ℝ

instance instTopologicalDivisionRingReal : TopologicalDivisionRing ℝ

instance EReal.instContinuousNeg : ContinuousNeg EReal

Instances for the following typeclasses are defined:

• IsTopologicalSemiring ℝ≥0
• ContinuousSub ℝ≥0
• HasContinuousInv₀ ℝ≥0 (continuity of x⁻¹ away from 0)
• ContinuousSMul ℝ≥0 α (whenever α has a continuous MulAction ℝ α)

Everything is inherited from the corresponding structures on the reals.

instance NNReal.instIsTopologicalSemiring : IsTopologicalSemiring NNReal

instance NNReal.instContinuousSub : ContinuousSub NNReal

instance NNReal.instHasContinuousInv₀ : HasContinuousInv₀ NNReal

instance NNReal.instContinuousSMulOfReal {α : Type u_1} [TopologicalSpace α] [MulAction ℝ α] [ContinuousSMul ℝ α] : ContinuousSMul NNReal α

theorem ENNReal.isEmbedding_coe : Topology.IsEmbedding ofNNReal

theorem ENNReal.tendsto_coe {α : Type u} {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 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