Theorems · Theorem · general topology

Equicontinuous.comap_uniformFun_eq

∀ {ι : Type u_1} {X : Type u_2} {α : Type u_3} [inst : TopologicalSpace X] [inst_1 : UniformSpace α] {F : ι → X → α}
  [CompactSpace X],
  Equicontinuous F →
    UniformSpace.comap F (UniformFun.uniformSpace X α) = UniformSpace.comap F (Pi.uniformSpace fun i => α)

Let X be a compact topological space, α a uniform space, and F : ι → (X → α) an equicontinuous family. Then, the uniform structures of uniform convergence and pointwise convergence induce the same uniform structure on ι. In other words, pointwise convergence and uniform convergence coincide on an equicontinuous subset of X → α. Consider using Equicontinuous.isUniformInducing_uniformFun_iff_pi and Equicontinuous.inducing_uniformFun_iff_pi instead, to avoid rewriting instances.

Defined in

Mathlib.Topology.UniformSpace.Ascoli

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceUniformSpaceCompactSpace