Theorems · Theorem · general topology

BoundedContinuousFunction.exists_extension_forall_exists_le_ge_of_isClosedEmbedding

∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [NormalSpace Y] [Nonempty X]
  (f : BoundedContinuousFunction X ℝ) {e : X → Y},
  Topology.IsClosedEmbedding e → ∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Set.Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f

Tietze extension theorem for real-valued bounded continuous maps, a version for a closed embedding. Let e be a closed embedding of a nonempty topological space X into a normal topological space Y. Let f be a bounded continuous real-valued function on X. Then there exists a bounded continuous function g : Y →ᵇ ℝ such that g ∘ e = f and each value g y belongs to a closed interval [f x₁, f x₂] for some x₁ and x₂.

Defined in

Mathlib.Topology.TietzeExtension

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceNormalSpaceNonempty