Theorems · Theorem · general topology

ContinuousMap.exists_forall_mem_restrict_eq

∀ {X : Type u} [inst : TopologicalSpace X] [NormalSpace X] {s : Set X},
  IsClosed s →
    ∀ {Y : Type v} [inst_2 : TopologicalSpace Y] (f : C(↑s, Y)) {t : Set Y},
      (∀ (x : ↑s), f x ∈ t) → ∀ [ht : TietzeExtension ↑t], ∃ g, (∀ (x : X), g x ∈ t) ∧ ContinuousMap.restrict s g = 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

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceNormalSpaceTopologicalSpaceTietzeExtension