Theorems · Theorem · general topology

EquicontinuousOn.tendsto_uniformOnFun_iff_pi

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

Let X be a topological space, 𝔖 a covering of X by compact subsets, α a uniform space, F : ι → (X → α) a family equicontinuous on each K ∈ 𝔖, and ℱ a filter on ι. Then, F tends to f : X → α along ℱ uniformly on each `K ∈ 𝔖` iff it tends to f pointwise along ℱ. This is a specialization of EquicontinuousOn.tendsto_uniformOnFun_iff_pi' to the case where 𝔖 covers X.

Defined in

Mathlib.Topology.UniformSpace.Ascoli

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceUniformSpace