Theorems · Theorem · general topology

uniformEquicontinuous_iff_uniformContinuous

∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {F : ι → β → α},
  UniformEquicontinuous F ↔ UniformContinuous (⇑UniformFun.ofFun ∘ Function.swap F)

A family 𝓕 : ι → β → α is uniformly equicontinuous iff the function swap 𝓕 : β → ι → α is uniformly continuous when `ι → α` is equipped with the uniform structure of uniform convergence. This is very useful for developing the equicontinuity API, but it should not be used directly for other purposes.

Defined in

Mathlib.Topology.UniformSpace.Equicontinuity

Cited by

9 results in Mathlib

Foundations

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

Assumes

UniformSpaceUniformSpace