English
One step in the iterative construction proving the Tietze extension theorem for real-valued bounded continuous maps with closed embeddings.
Русский
Один шаг итеративной конструкции доказательства теоремы Титце для вещественных ограниченно непрерывных отображений с замкнутыми внедрениями.
LaTeX
$$$\\exists\\ g:\\ Y \\to \\mathbb{R},\\; \\|g\\| \\\\le \\\\tfrac{2}{3}\\\\|f\\\\| \\text{ и } dist(g \\circ e, f) \\\\le \\\\tfrac{2}{3} \\,\\\\|f\\\\|$$$
Lean4
/-- Any homeomorphism from a `TietzeExtension` space is one itself. -/
theorem of_homeo {Y : Type v} {Z : Type w} [TopologicalSpace Y] [TopologicalSpace Z] [TietzeExtension.{u, w} Z]
(e : Y ≃ₜ Z) : TietzeExtension.{u, v} Y :=
.of_retract (e : C(Y, Z)) (e.symm : C(Z, Y)) <| by simp
