Theorems · Theorem · general topology

ContinuousMap.exists_extension

∀ {X₁ : Type u₁} [inst : TopologicalSpace X₁] {X : Type u} [inst_1 : TopologicalSpace X] [NormalSpace X] {e : X₁ → X}
  {Y : Type v} [inst_3 : TopologicalSpace Y] [TietzeExtension Y] (he : Topology.IsClosedEmbedding e) (f : C(X₁, Y)),
  ∃ g, g.comp { toFun := e, continuous_toFun := ⋯ } = f

Tietze extension theorem for TietzeExtension spaces. Let e be a closed embedding of a nonempty topological space X₁ into a normal topological space X. Let f be a continuous function on X₁ with values in a TietzeExtension space Y. Then there exists a continuous function g : C(X, Y) such that g ∘ e = f.

Defined in

Mathlib.Topology.TietzeExtension

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceNormalSpaceTopologicalSpaceTietzeExtension