Theorems · Theorem · general topology

ContinuousMap.exists_restrict_eq

∀ {X : Type u} [inst : TopologicalSpace X] [NormalSpace X] {s : Set X} {Y : Type v} [inst_2 : TopologicalSpace Y]
  [TietzeExtension Y], IsClosed s → ∀ (f : C(↑s, Y)), ∃ g, ContinuousMap.restrict s g = f

Tietze extension theorem for TietzeExtension spaces, a version for a closed set. Let s be a closed set in a normal topological space X. Let f be a continuous function on s with values in a TietzeExtension space Y. Then there exists a continuous function g : C(X, Y) such that g.restrict s = f.

Defined in

Mathlib.Topology.TietzeExtension

Cited by

3 results in Mathlib

Foundations

Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceNormalSpaceTopologicalSpaceTietzeExtension