English
Tietze extension theorem for real-valued bounded maps on a closed set within a normal space.
Русский
Теорема Титце о продолжении для вещественных ограниченно непрерывных отображений на замкнутом подмножестве пространства.
LaTeX
$$$\\exists g:\\ Y \\to \\mathbb{R}, \\; \\|g\\| = \\|f\\| \\land g\\restriction s = f$$$
Lean4
/-- **Tietze extension theorem** for real-valued bounded continuous maps, a version for a closed
set. Let `s` be a closed set in a normal topological space `Y`. Let `f` be a bounded continuous
real-valued function on `s`. 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 : s`. Then there exists a bounded continuous real-valued function
`g : Y →ᵇ ℝ` such that `g y ∈ t` for all `y` and `g.restrict s = f`. -/
theorem exists_forall_mem_restrict_eq_of_closed {s : Set Y} (f : s →ᵇ ℝ) (hs : IsClosed s) {t : Set ℝ} [OrdConnected t]
(hf : ∀ x, f x ∈ t) (hne : t.Nonempty) : ∃ g : Y →ᵇ ℝ, (∀ y, g y ∈ t) ∧ g.restrict s = f :=
by
obtain ⟨g, hg, hgf⟩ := exists_extension_forall_mem_of_isClosedEmbedding f hf hne hs.isClosedEmbedding_subtypeVal
exact ⟨g, hg, DFunLike.coe_injective hgf⟩
