Theorems · Theorem · general topology

EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi

∀ {ι : Type u_1} {X : Type u_2} {α : Type u_3} [inst : TopologicalSpace X] [inst_1 : UniformSpace α] {F : ι → X → α}
  [inst_2 : UniformSpace ι] {𝔖 : Set (Set X)},
  ⋃₀ 𝔖 = Set.univ →
    (∀ K ∈ 𝔖, IsCompact K) →
      (∀ K ∈ 𝔖, EquicontinuousOn F K) → (IsUniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsUniformInducing F)

Let X be a topological space, 𝔖 a covering of X by compact subsets, α a uniform space, and F : ι → (X → α) a family which is equicontinuous on each K ∈ 𝔖. Then, the uniform structures of uniform convergence on 𝔖 and pointwise convergence induce the same uniform structure on ι. This is a specialization of EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi' to the case where 𝔖 covers X.

Defined in

Mathlib.Topology.UniformSpace.Ascoli

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceUniformSpaceUniformSpace