coeNNRealReal — Mathlib

English

There is a natural embedding of NNReal into Real as a continuous map.

Русский

Существует естественное вложение NNReal в Real как непрерывное отображение.

LaTeX

$$$\\text{ContinuousMap.coeNNRealReal} : C(\\mathbb{R}_{\\ge 0}, \\mathbb{R})$$$

Lean4

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

Похожие утверждения