Theorems · Theorem · general topology

Metric.uniformEquicontinuous_iff

∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] {ι : Type u_4} [inst_1 : PseudoMetricSpace β]
  {F : ι → β → α},
  UniformEquicontinuous F ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε

Characterization of uniform equicontinuity for families of functions between (pseudo) metric spaces.

Defined in

Mathlib.Topology.MetricSpace.Equicontinuity

Cited by

1 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpacePseudoMetricSpace