Mathlib.Topology.UniformSpace.Real

Module docstring

{"# 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. ","### Topology on ℝ≥0 All the instances are inherited from the corresponding structures on the reals.

Real.instCompleteSpace instance

: CompleteSpace ℝ

Full source

instance Real.instCompleteSpace : CompleteSpace ℝ := by
  apply complete_of_cauchySeq_tendsto
  intro u hu
  let c : CauSeq ℝ abs := ⟨u, Metric.cauchySeq_iff'.1 hu⟩
  refine ⟨c.lim, fun s h => ?_⟩
  rcases Metric.mem_nhds_iff.1 h with ⟨ε, ε0, hε⟩
  have := c.equiv_lim ε ε0
  simp only [mem_map, mem_atTop_sets, mem_setOf_eq]
  exact this.imp fun N hN n hn => hε (hN n hn)

Completeness of the Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a complete space.

NNReal.instTopologicalSpace instance

: TopologicalSpace ℝ≥0

Full source

instance : TopologicalSpace ℝ≥0 := inferInstance

Topological Space Structure on Nonnegative Reals

Informal description

The nonnegative real numbers $\mathbb{R}_{\geq 0}$ are equipped with the topological space structure induced from the real numbers $\mathbb{R}$.

NNReal.instCompleteSpace instance

: CompleteSpace ℝ≥0

Full source

instance : CompleteSpace ℝ≥0 :=
  isClosed_Ici.completeSpace_coe

Completeness of Nonnegative Real Numbers

Informal description

The nonnegative real numbers $\mathbb{R}_{\geq 0}$ form a complete space.

NNReal.continuous_coe theorem

: Continuous ((↑) : ℝ≥0 → ℝ)

Full source

theorem continuous_coe : Continuous ((↑) : ℝ≥0 → ℝ) :=
  continuous_subtype_val

Continuity of the Nonnegative Real Embedding

Informal description

The canonical embedding from the nonnegative real numbers $\mathbb{R}_{\geq 0}$ to the real numbers $\mathbb{R}$ is continuous.

ContinuousMap.coeNNRealReal definition

: C(ℝ≥0, ℝ)

Full source

/-- Embedding of `ℝ≥0` to `ℝ` as a bundled continuous map. -/
@[simps -fullyApplied]
def _root_.ContinuousMap.coeNNRealReal : C(ℝ≥0, ℝ) :=
  ⟨(↑), continuous_coe⟩

Continuous embedding of nonnegative reals into reals

Informal description

The canonical embedding from the nonnegative real numbers $\mathbb{R}_{\geq 0}$ to the real numbers $\mathbb{R}$, viewed as a continuous map.

NNReal.coeNNRealReal_zero theorem

: ContinuousMap.coeNNRealReal 0 = 0

Full source

@[simp]
lemma coeNNRealReal_zero : ContinuousMap.coeNNRealReal 0 = 0 := rfl

Embedding Preserves Zero: $\text{coeNNRealReal}(0) = 0$

Informal description

The continuous embedding of the nonnegative real numbers into the reals maps $0$ to $0$, i.e., $\text{coeNNRealReal}(0) = 0$.

NNReal.ContinuousMap.canLift instance

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

Full source

instance ContinuousMap.canLift {X : Type*} [TopologicalSpace X] :
    CanLift C(X, ℝ) C(X, ℝ≥0) ContinuousMap.coeNNRealReal.comp fun f => ∀ x, 0 ≤ f x where
  prf f hf := ⟨⟨fun x => ⟨f x, hf x⟩, f.2.subtype_mk _⟩, DFunLike.ext' rfl⟩

Lifting Condition for Nonnegative Continuous Functions

Informal description

For any topological space $X$, there exists a lifting condition from continuous functions $X \to \mathbb{R}$ to continuous functions $X \to \mathbb{R}_{\geq 0}$, where the lifting is performed via composition with the canonical embedding $\mathbb{R}_{\geq 0} \hookrightarrow \mathbb{R}$ and the condition requires that the function is nonnegative everywhere.