Theorems · Theorem · general topology

Equicontinuous.isUniformInducing_uniformFun_iff_pi

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

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 → α. This is a version of Equicontinuous.comap_uniformFun_eq stated in terms of IsUniformInducing for convenience.

Defined in

Mathlib.Topology.UniformSpace.Ascoli

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceUniformSpaceUniformSpaceCompactSpace