Documentation

Mathlib.Topology.UniformSpace.Real

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.

source
instance Real.instCompleteSpace :
CompleteSpace ℝ

Topology on ℝ≥0 #

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

source
instance NNReal.instTopologicalSpace :
TopologicalSpace NNReal
Equations
    source
    instance NNReal.instCompleteSpace :
    CompleteSpace NNReal
    source
    theorem NNReal.continuous_coe :
    Continuous toReal
    source
    def ContinuousMap.coeNNRealReal :
    C(NNReal, ℝ)

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

    Equations
      Instances For
        source
        @[simp]
        theorem ContinuousMap.coeNNRealReal_apply :
        ⇑coeNNRealReal = NNReal.toReal
        source
        @[simp]
        theorem NNReal.coeNNRealReal_zero :
        ContinuousMap.coeNNRealReal 0 = 0
        source
        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