Topological properties of ℝ

instance instNoncompactSpaceReal : NoncompactSpace ℝ

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

theorem Real.uniformContinuous_neg : UniformContinuous Neg.neg

instance instUniformAddGroupReal : UniformAddGroup ℝ

instance instTopologicalAddGroupReal : TopologicalAddGroup ℝ

instance instTopologicalRingReal : TopologicalRing ℝ

instance instTopologicalDivisionRingReal : TopologicalDivisionRing ℝ

instance instProperSpaceReal : ProperSpace ℝ

instance instSecondCountableTopologyReal : SecondCountableTopology ℝ

instance Real.instCompleteSpace : CompleteSpace ℝ

instance instIsOrderBornology : IsOrderBornology ℝ

instance instContinuousStarReal : ContinuousStar ℝ