The reals are complete

This file provides the instances CompleteSpace ℝ and CompleteSpace ℝ≥0. Along the way, we add a shortcut instance for the natural topology on ℝ≥0 (the one induced from ℝ), and add some basic API.

instance Real.instCompleteSpace : CompleteSpace ℝ

Topology on ℝ≥0

All the instances are inherited from the corresponding structures on the reals.

instance NNReal.instTopologicalSpace : TopologicalSpace NNReal

Equations

• NNReal.instTopologicalSpace = inferInstance

instance NNReal.instCompleteSpace : CompleteSpace NNReal

theorem NNReal.continuous_coe : Continuous toReal

def ContinuousMap.coeNNRealReal : C(NNReal, ℝ)

Embedding of ℝ≥0 to ℝ as a bundled continuous map.

Equations

• ContinuousMap.coeNNRealReal = { toFun := NNReal.toReal, continuous_toFun := NNReal.continuous_coe }

@[simp]

theorem ContinuousMap.coeNNRealReal_apply : ⇑coeNNRealReal = NNReal.toReal

@[simp]

theorem NNReal.coeNNRealReal_zero : ContinuousMap.coeNNRealReal 0 = 0

instance NNReal.ContinuousMap.canLift {X : Type u_1} [TopologicalSpace X] : CanLift C(X, ℝ) C(X, NNReal) ContinuousMap.coeNNRealReal.comp fun (f : C(X, ℝ)) => ∀ (x : X), 0 ≤ f x