Theorems · Definition · general topology

UniformEquicontinuous

{ι : Type u_1} → {α : Type u_6} → {β : Type u_8} → [uα : UniformSpace α] → [uβ : UniformSpace β] → (ι → β → α) → Prop

A family F : ι → β → α of functions between uniform spaces is uniformly equicontinuous if, for all entourages U ∈ 𝓤 α, there is an entourage V ∈ 𝓤 β such that, whenever x and y are V-close, we have that, for all `i : ι`, F i x is U-close to F i y.

Defined in

Mathlib.Topology.UniformSpace.Equicontinuity

Cited by

35 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

UniformSpaceUniformSpace