Theorems · Definition · general topology

UniformEquicontinuousOn

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

A family F : ι → β → α of functions between uniform spaces is uniformly equicontinuous on `S : Set β` if, for all entourages U ∈ 𝓤 α, there is a relative entourage V ∈ 𝓤 β ⊓ 𝓟 (S ×ˢ S) 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

21 results in Mathlib

Foundations

Depth 48 from the axioms · uses propext, Quot.sound

Assumes

UniformSpaceUniformSpace