English
Let s be a closed subset of a normal space Y. Let f: s → ℝ be continuous, and let t ⊆ ℝ be a nonempty convex (OrdConnected) set such that f(x) ∈ t for all x ∈ s. Then there exists a continuous g: Y → ℝ with g(y) ∈ t for all y ∈ Y, and g restricted to s equals f.
Русский
Пусть s — замкнутое подмножество нормального пространства Y. Пусть f: s → ℝ непрерывна, и пусть t ⊆ ℝ — непустое выпуклое множество (в смысле OrdConnected), такое что f(x) ∈ t для всех x ∈ s. Тогда существует непрерывная функция g: Y → ℝ, такая что g(y) ∈ t для всех y и ограничение g на s равно f.
LaTeX
$$$\\exists g : C(Y, \\mathbb{R}), (\\forall y \\in Y, g(y) \\in t) \\land g|_s = f$$$
Lean4
/-- **Tietze extension theorem** for real-valued continuous maps, a version for a closed set. Let
`s` be a closed set in a normal topological space `Y`. Let `f` be a 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 continuous real-valued function `g : C(Y, ℝ)` such that `g y ∈ t` for all `y` and
`g.restrict s = f`. -/
theorem exists_restrict_eq_forall_mem_of_closed {s : Set Y} (f : C(s, ℝ)) {t : Set ℝ} [OrdConnected t]
(ht : ∀ x, f x ∈ t) (hne : t.Nonempty) (hs : IsClosed s) : ∃ g : C(Y, ℝ), (∀ y, g y ∈ t) ∧ g.restrict s = f :=
let ⟨g, hgt, hgf⟩ := exists_extension_forall_mem_of_isClosedEmbedding f ht hne hs.isClosedEmbedding_subtypeVal
⟨g, hgt, coe_injective hgf⟩
