Theorems · Theorem · general topology

ContinuousMap.exists_extension_forall_mem

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

This theorem is not intended to be used directly because it is rare for a set alone to satisfy [TietzeExtension t]. For example, Metric.ball in ℝ only satisfies it when the radius is strictly positive, so finding this as an instance will fail. Instead, it is intended to be used as a constructor for theorems about sets which do satisfy [TietzeExtension t] under some hypotheses.

Defined in

Mathlib.Topology.TietzeExtension

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceNormalSpaceTopologicalSpaceTietzeExtension