Theorems · Theorem · general topology

ContinuousMap.isComplete_setOfPred_eqOn

∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] [CompleteSpace C(α, β)] (f : α → β)
  (s : Set α), IsComplete {g | Set.EqOn (⇑g) f s}

If C(α, β) is a complete space, then for any (possibly, discontinuous) function f and any set s, the set of functions g : C(α, β) that are equal to f on s is a complete set. Note that this set does not have to be a closed set when β is not T0. This lemma is useful to prove that, e.g., the space of paths between two points and the space of homotopies between two continuous maps are complete spaces, without assuming that the codomain is a Hausdorff space.

Defined in

Mathlib.Topology.UniformSpace.CompactConvergence

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceUniformSpaceCompleteSpace