English
Nonnegative real numbers ℝ≥0 admit the Tietze extension property: any continuous map from a closed subset into ℝ≥0 extends to a continuous map on the whole space with values in ℝ≥0.
Русский
Неотрицательные вещественные числа ℝ≥0 обладают свойством расширения Титце: любая непрерывная функция с замкнутого множества в ℝ≥0 может быть непрерывно продолжена на все пространство с значениями в ℝ≥0.
LaTeX
$$$\\text{TietzeExtension}(\\mathbb{R}_{\\ge 0})$$$
Lean4
/-- **Tietze extension theorem** for nonnegative real-valued continuous maps.
`ℝ≥0` is a `TietzeExtension` space. -/
instance instTietzeExtension : TietzeExtension ℝ≥0 :=
.of_retract ⟨((↑) : ℝ≥0 → ℝ), by continuity⟩ ⟨Real.toNNReal, continuous_real_toNNReal⟩ <| by ext; simp
