Theorems · Theorem · general topology

UniformOnFun.isClosed_setOfPred_continuous

∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] {𝔖 : Set (Set α)} [inst_1 : TopologicalSpace α],
  Topology.IsCoherentWith 𝔖 → IsClosed {f | Continuous ((UniformOnFun.toFun 𝔖) f)}

Suppose that the topology on α is defined by its restrictions to the sets of 𝔖. Then the set of continuous functions is closed in the topology of uniform convergence on the sets of 𝔖.

Defined in

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Cited by

3 results in Mathlib

Foundations

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

Assumes

UniformSpaceTopologicalSpace