Theorems · Theorem · general topology

Equicontinuous.inducing_uniformFun_iff_pi

∀ {ι : Type u_1} {X : Type u_2} {α : Type u_3} [inst : TopologicalSpace X] [inst_1 : UniformSpace α] {F : ι → X → α}
  [inst_2 : TopologicalSpace ι] [CompactSpace X],
  Equicontinuous F → (Topology.IsInducing (⇑UniformFun.ofFun ∘ F) ↔ Topology.IsInducing F)

Let X be a compact topological space, α a uniform space, and F : ι → (X → α) an equicontinuous family. Then, the topologies of uniform convergence and pointwise convergence induce the same topology on ι. In other words, pointwise convergence and uniform convergence coincide on an equicontinuous subset of X → α. This is a consequence of Equicontinuous.comap_uniformFun_eq, stated in terms of IsInducing for convenience.

Defined in

Mathlib.Topology.UniformSpace.Ascoli

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceUniformSpaceTopologicalSpaceCompactSpace