Theorems · Theorem · general topology

uniformEquicontinuousOn_iff_uniformContinuousOn

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

A family 𝓕 : ι → β → α is uniformly equicontinuous on S iff the function swap 𝓕 : β → ι → α is uniformly continuous on S 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

6 results in Mathlib

Foundations

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

Assumes

UniformSpaceUniformSpace