Theorems · Theorem · general topology

Filter.Tendsto.uniformContinuous_of_uniformEquicontinuous

∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {l : Filter ι} [l.NeBot]
  {F : ι → β → α} {f : β → α}, Filter.Tendsto F l (nhds f) → UniformEquicontinuous F → UniformContinuous f

If 𝓕 : ι → β → α tends to f : β → α pointwise along some nontrivial filter, and if the family 𝓕 is uniformly equicontinuous, then the limit is uniformly continuous.

Defined in

Mathlib.Topology.UniformSpace.Equicontinuity

Cited by

0 results in Mathlib

Foundations

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

Assumes

UniformSpaceUniformSpaceFilter.NeBot