# Equicontinuity of a family of functions #

Let `X`

be a topological space and `α`

a `UniformSpace`

. A family of functions `F : ι → X → α`

is said to be *equicontinuous at a point x₀ : X* when, for any entourage

`U`

in `α`

, there is a
neighborhood `V`

of `x₀`

such that, for all `x ∈ V`

, and *for all*,

`i`

`F i x`

is `U`

-close to
`F i x₀`

. In other words, one has `∀ U ∈ 𝓤 α, ∀ᶠ x in 𝓝 x₀, ∀ i, (F i x₀, F i x) ∈ U`

.
For maps between metric spaces, this corresponds to
`∀ ε > 0, ∃ δ > 0, ∀ x, ∀ i, dist x₀ x < δ → dist (F i x₀) (F i x) < ε`

.`F`

is said to be *equicontinuous* if it is equicontinuous at each point.

A closely related concept is that of **uniform***equicontinuity* of a family of functions
`F : ι → β → α`

between uniform spaces, which means that, for any entourage `U`

in `α`

, there is an
entourage `V`

in `β`

such that, if `x`

and `y`

are `V`

-close, then *for all i*,

`F i x`

and
`F i y`

are `U`

-close. In other words, one has
`∀ U ∈ 𝓤 α, ∀ᶠ xy in 𝓤 β, ∀ i, (F i xy.1, F i xy.2) ∈ U`

.
For maps between metric spaces, this corresponds to
`∀ ε > 0, ∃ δ > 0, ∀ x y, ∀ i, dist x y < δ → dist (F i x₀) (F i x) < ε`

.## Main definitions #

`EquicontinuousAt`

: equicontinuity of a family of functions at a point`Equicontinuous`

: equicontinuity of a family of functions on the whole domain`UniformEquicontinuous`

: uniform equicontinuity of a family of functions on the whole domain

## Main statements #

`equicontinuous_iff_continuous`

: equicontinuity can be expressed as a simple continuity condition between well-chosen function spaces. This is really useful for building up the theory.`Equicontinuous.closure`

: if a set of functions is equicontinuous, its closure*for the topology of uniform convergence*is also equicontinuous.

## Notations #

Throughout this file, we use :

`ι`

,`κ`

for indexing types`X`

,`Y`

,`Z`

for topological spaces`α`

,`β`

,`γ`

for uniform spaces

## Implementation details #

We choose to express equicontinuity as a properties of indexed families of functions rather than sets of functions for the following reasons:

- it is really easy to express equicontinuity of
`H : Set (X → α)`

using our setup: it is just equicontinuity of the family`(↑) : ↥H → (X → α)`

. On the other hand, going the other way around would require working with the range of the family, which is always annoying because it introduces useless existentials. - in most applications, one doesn't work with bare functions but with a more specific hom type
`hom`

. Equicontinuity of a set`H : Set hom`

would then have to be expressed as equicontinuity of`coe_fn '' H`

, which is super annoying to work with. This is much simpler with families, because equicontinuity of a family`𝓕 : ι → hom`

would simply be expressed as equicontinuity of`coe_fn ∘ 𝓕`

, which doesn't introduce any nasty existentials.

To simplify statements, we do provide abbreviations `Set.EquicontinuousAt`

, `Set.Equicontinuous`

and `Set.UniformEquicontinuous`

asserting the corresponding fact about the family
`(↑) : ↥H → (X → α)`

where `H : Set (X → α)`

. Note however that these won't work for sets of hom
types, and in that case one should go back to the family definition rather than using `Set.image`

.

Since we have no use case for it yet, we don't introduce any relative version
(i.e no `EquicontinuousWithinAt`

or `EquicontinuousOn`

), but this is more of a conservative
position than a design decision, so anyone needing relative versions should feel free to add them,
and that should hopefully be a straightforward task.

## References #

- [N. Bourbaki,
*General Topology, Chapter X*][bourbaki1966]

## Tags #

equicontinuity, uniform convergence, ascoli

A family `F : ι → X → α`

of functions from a topological space to a uniform space is
*equicontinuous at x₀ : X* if, for all entourage

`U ∈ 𝓤 α`

, there is a neighborhood `V`

of `x₀`

such that, for all `x ∈ V`

and for all `i : ι`

, `F i x`

is `U`

-close to `F i x₀`

.## Instances For

We say that a set `H : Set (X → α)`

of functions is equicontinuous at a point if the family
`(↑) : ↥H → (X → α)`

is equicontinuous at that point.

## Instances For

A family `F : ι → X → α`

of functions from a topological space to a uniform space is
*equicontinuous* on all of `X`

if it is equicontinuous at each point of `X`

.

## Instances For

We say that a set `H : Set (X → α)`

of functions is equicontinuous if the family
`(↑) : ↥H → (X → α)`

is equicontinuous.

## Instances For

A family `F : ι → β → α`

of functions between uniform spaces is *uniformly equicontinuous* if,
for all entourage `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 x₀`

.## Instances For

We say that a set `H : Set (X → α)`

of functions is uniformly equicontinuous if the family
`(↑) : ↥H → (X → α)`

is uniformly equicontinuous.

## Instances For

### Empty index type #

### Finite index type #

### Index type with a unique element #

Reformulation of equicontinuity at `x₀`

comparing two variables near `x₀`

instead of comparing
only one with `x₀`

.

Uniform equicontinuity implies equicontinuity.

Each function of a family equicontinuous at `x₀`

is continuous at `x₀`

.

Each function of an equicontinuous family is continuous.

Each function of a uniformly equicontinuous family is uniformly continuous.

Taking sub-families preserves equicontinuity at a point.

Taking sub-families preserves equicontinuity.

Taking sub-families preserves uniform equicontinuity.

A family `𝓕 : ι → X → α`

is equicontinuous at `x₀`

iff `range 𝓕`

is equicontinuous at `x₀`

,
i.e the family `(↑) : range F → X → α`

is equicontinuous at `x₀`

.

A family `𝓕 : ι → X → α`

is equicontinuous iff `range 𝓕`

is equicontinuous,
i.e the family `(↑) : range F → X → α`

is equicontinuous.

A family `𝓕 : ι → β → α`

is uniformly equicontinuous iff `range 𝓕`

is uniformly equicontinuous,
i.e the family `(↑) : range F → β → α`

is uniformly equicontinuous.

A family `𝓕 : ι → X → α`

is equicontinuous at `x₀`

iff the function `swap 𝓕 : X → ι → α`

is
continuous at `x₀`

*when ι → α is equipped with the topology of uniform convergence*. This is
very useful for developping the equicontinuity API, but it should not be used directly for other
purposes.

A family `𝓕 : ι → X → α`

is equicontinuous iff the function `swap 𝓕 : X → ι → α`

is
continuous *when ι → α is equipped with the topology of uniform convergence*. This is
very useful for developping the equicontinuity API, but it should not be used directly for other
purposes.

A family `𝓕 : ι → β → α`

is uniformly equicontinuous iff the function `swap 𝓕 : β → ι → α`

is
uniformly continuous *when ι → α is equipped with the uniform structure of uniform convergence*.
This is very useful for developping the equicontinuity API, but it should not be used directly
for other purposes.

Given `u : α → β`

a uniform inducing map, a family `𝓕 : ι → X → α`

is equicontinuous at a point
`x₀ : X`

iff the family `𝓕'`

, obtained by precomposing each function of `𝓕`

by `u`

, is
equicontinuous at `x₀`

.

Given `u : α → β`

a uniform inducing map, a family `𝓕 : ι → X → α`

is equicontinuous iff the
family `𝓕'`

, obtained by precomposing each function of `𝓕`

by `u`

, is equicontinuous.

Given `u : α → γ`

a uniform inducing map, a family `𝓕 : ι → β → α`

is uniformly equicontinuous
iff the family `𝓕'`

, obtained by precomposing each function of `𝓕`

by `u`

, is uniformly
equicontinuous.

A version of `EquicontinuousAt.closure`

applicable to subsets of types which embed continuously
into `X → α`

with the product topology. It turns out we don't need any other condition on the
embedding than continuity, but in practice this will mostly be applied to `FunLike`

types where
the coercion is injective.

If a set of functions is equicontinuous at some `x₀`

, its closure for the product topology is
also equicontinuous at `x₀`

.

If `𝓕 : ι → X → α`

tends to `f : X → α`

*pointwise* along some nontrivial filter, and if the
family `𝓕`

is equicontinuous at some `x₀ : X`

, then the limit is continuous at `x₀`

.

A version of `Equicontinuous.closure`

applicable to subsets of types which embed continuously
into `X → α`

with the product topology. It turns out we don't need any other condition on the
embedding than continuity, but in practice this will mostly be applied to `FunLike`

types where
the coercion is injective.

If a set of functions is equicontinuous, its closure for the product topology is also equicontinuous.

If `𝓕 : ι → X → α`

tends to `f : X → α`

*pointwise* along some nontrivial filter, and if the
family `𝓕`

is equicontinuous, then the limit is continuous.

A version of `UniformEquicontinuous.closure`

applicable to subsets of types which embed
continuously into `β → α`

with the product topology. It turns out we don't need any other condition
on the embedding than continuity, but in practice this will mostly be applied to `FunLike`

types
where the coercion is injective.

If a set of functions is uniformly equicontinuous, its closure for the product topology is also uniformly equicontinuous.

If `𝓕 : ι → β → α`

tends to `f : β → α`

*pointwise* along some nontrivial filter, and if the
family `𝓕`

is uniformly equicontinuous, then the limit is uniformly continuous.

If `F : ι → X → α`

is a family of functions equicontinuous at `x`

,
it tends to `f y`

along a filter `l`

for any `y ∈ s`

,
the limit function `f`

tends to `z`

along `𝓝[s] x`

, and `x ∈ closure s`

,
then `(F · x)`

tends to `z`

along `l`

.

In some sense, this is a converse of `EquicontinuousAt.closure`

.

If `F : ι → X → α`

is an equicontinuous family of functions,
`f : X → α`

is a continuous function, and `l`

is a filter on `ι`

,
then `{x | Filter.Tendsto (F · x) l (𝓝 (f x))}`

is a closed set.