English
Any homeomorphism between TietzeExtension spaces preserves the extension structure.
Русский
Любой гомеоморфизм между пространствами TietzeExtension сохраняет структуру расширения.
LaTeX
$$$\\forall e:\\ Y \\simeq_t Z,\\ [\\mathrm{TietzeExtension}(Z)] \\Rightarrow \\mathrm{TietzeExtension}(Y)$$$
Lean4
/-- **Tietze extension theorem** for real-valued bounded continuous maps, a version for a closed
embedding. Let `e` be a closed embedding of a nonempty topological space `X` into a normal
topological space `Y`. Let `f` be a bounded continuous real-valued function on `X`. Let `t` be
a nonempty convex set of real numbers (we use `OrdConnected` instead of `Convex` to automatically
deduce this argument by typeclass search) such that `f x ∈ t` for all `x`. Then there exists
a bounded continuous real-valued function `g : Y →ᵇ ℝ` such that `g y ∈ t` for all `y` and
`g ∘ e = f`. -/
theorem exists_extension_forall_mem_of_isClosedEmbedding (f : X →ᵇ ℝ) {t : Set ℝ} {e : X → Y} [hs : OrdConnected t]
(hf : ∀ x, f x ∈ t) (hne : t.Nonempty) (he : IsClosedEmbedding e) : ∃ g : Y →ᵇ ℝ, (∀ y, g y ∈ t) ∧ g ∘ e = f :=
by
cases isEmpty_or_nonempty X
· rcases hne with ⟨c, hc⟩
exact ⟨const Y c, fun _ => hc, funext fun x => isEmptyElim x⟩
rcases exists_extension_forall_exists_le_ge_of_isClosedEmbedding f he with ⟨g, hg, hgf⟩
refine ⟨g, fun y => ?_, hgf⟩
rcases hg y with ⟨xl, xu, h⟩
exact hs.out (hf _) (hf _) h
