Tietze extension with prescribed constant values

Let e : X₁ → X be a closed embedding into a normal space and let s and t be disjoint closed subsets of X. A continuous function f on X₁ with values in a space satisfying the Tietze extension property, equal to a on e ⁻¹' s and to b on e ⁻¹' t, extends along e to a continuous function on X equal to a on all of s and to b on all of t (ContinuousMap.exists_extension_eqOn_const). For X₁ empty this is Urysohn's lemma.

This relative form of Urysohn's lemma is what proves normality of spaces built by attaching: a separating function on the old space is extended over the attached space while it separates the traces of two closed sets there.

References

• J. R. Munkres, Topology, 2nd ed., Prentice Hall (2000), §35, Theorem 35.1.

theorem ContinuousMap.exists_extension_eqOn_const {X₁ : Type u₁} [TopologicalSpace X₁] {X : Type u} [TopologicalSpace X] [NormalSpace X] {Y : Type v} [TopologicalSpace Y] [TietzeExtension Y] {e : X₁ → X} (he : Topology.IsClosedEmbedding e) (f : C(X₁, Y)) {s t : Set X} (hs : IsClosed s) (ht : IsClosed t) (hst : Disjoint s t) {a b : Y} (hfs : Set.EqOn (⇑f) (fun (x : X₁) => a) (e ⁻¹' s)) (hft : Set.EqOn (⇑f) (fun (x : X₁) => b) (e ⁻¹' t)) : ∃ (g : C(X, Y)), ⇑g ∘ e = ⇑f ∧ Set.EqOn (⇑g) (fun (x : X) => a) s ∧ Set.EqOn (⇑g) (fun (x : X) => b) t

Tietze extension with prescribed values. Let e be a closed embedding into a normal space and let s and t be disjoint closed sets. A continuous function f equal to a on e ⁻¹' s and to b on e ⁻¹' t extends along e to a continuous function equal to a on s and to b on t.