# Equicontinuity in metric spaces #

This files contains various facts about (uniform) equicontinuity in metric spaces. Most
importantly, we prove the usual characterization of equicontinuity of `F`

at `x₀`

in the case of
(pseudo) metric spaces: `∀ ε > 0, ∃ δ > 0, ∀ x, dist x x₀ < δ → ∀ i, dist (F i x₀) (F i x) < ε`

,
and we prove that functions sharing a common (local or global) continuity modulus are
(locally or uniformly) equicontinuous.

## Main statements #

`Metric.equicontinuousAt_iff`

: characterization of equicontinuity for families of functions between (pseudo) metric spaces.`Metric.equicontinuousAt_of_continuity_modulus`

: convenient way to prove equicontinuity at a point of a family of functions to a (pseudo) metric space by showing that they share a common*local*continuity modulus.`Metric.uniformEquicontinuous_of_continuity_modulus`

: convenient way to prove uniform equicontinuity of a family of functions to a (pseudo) metric space by showing that they share a common*global*continuity modulus.

## Tags #

equicontinuity, continuity modulus

Characterization of equicontinuity for families of functions taking values in a (pseudo) metric space.

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

Reformulation of `equicontinuousAt_iff_pair`

for families of functions taking values in a
(pseudo) metric space.

Characterization of uniform equicontinuity for families of functions taking values in a (pseudo) metric space.

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

For a family of functions to a (pseudo) metric spaces, a convenient way to prove
equicontinuity at a point is to show that all of the functions share a common *local* continuity
modulus.

For a family of functions between (pseudo) metric spaces, a convenient way to prove
uniform equicontinuity is to show that all of the functions share a common *global* continuity
modulus.

For a family of functions between (pseudo) metric spaces, a convenient way to prove
equicontinuity is to show that all of the functions share a common *global* continuity modulus.