Topology on ℝ≥0

The natural topology on ℝ≥0 (the one induced from ℝ), and a basic API.

Main definitions

Instances for the following typeclasses are defined:

• TopologicalSpace ℝ≥0
• TopologicalSemiring ℝ≥0
• SecondCountableTopology ℝ≥0
• OrderTopology ℝ≥0
• ProperSpace ℝ≥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.instTopologicalSpace : TopologicalSpace NNReal

Equations

• NNReal.instTopologicalSpace = inferInstance

instance NNReal.instTopologicalSemiring : TopologicalSemiring NNReal

instance NNReal.instSecondCountableTopology : SecondCountableTopology NNReal

instance NNReal.instOrderTopology : OrderTopology NNReal

instance NNReal.instCompleteSpace : CompleteSpace NNReal

instance NNReal.instContinuousStar : ContinuousStar NNReal

instance NNReal.instIsOrderBornology : IsOrderBornology NNReal

theorem NNReal.continuous_coe : Continuous NNReal.toReal

instance NNReal.instContinuousSub : ContinuousSub NNReal

instance NNReal.instHasContinuousInv₀ : HasContinuousInv₀ NNReal

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

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 : ⇑ContinuousMap.coeNNRealReal = NNReal.toReal

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

instance NNReal.instProperSpace : ProperSpace NNReal