English
The real numbers ℝ enjoy the Tietze extension property: any continuous real-valued map defined on a closed subset of a normal space can be extended to a continuous map on the whole space, taking values in ℝ.
Русский
Числа ℝ обладают свойством расширения Титце: любая непрерывная функция с значениями в ℝ, определённая на замкнутом подмножестве нормального пространства, может быть продолжена на всё пространство непрерывной функцией с значениями в ℝ.
LaTeX
$$$\\text{TietzeExtension}(\\mathbb{R})$$$
Lean4
/-- **Tietze extension theorem** for real-valued continuous maps.
`ℝ` is a `TietzeExtension` space. -/
instance instTietzeExtension : TietzeExtension ℝ where
exists_restrict_eq' _s hs
f := f.exists_restrict_eq_forall_mem_of_closed (fun _ => mem_univ _) univ_nonempty hs |>.imp fun _ ↦ (And.right ·)
