# 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

We also introduce relative versions, namely `EquicontinuousWithinAt`

, `EquicontinuousOn`

and
`UniformEquicontinuousOn`

, akin to `ContinuousWithinAt`

, `ContinuousOn`

and `UniformContinuousOn`

respectively.

## 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 pointwise 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`

.

## References #

## 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 entourages

`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₀`

.## Equations

- EquicontinuousAt F x₀ = ∀ U ∈ uniformity α, ∀ᶠ (x : X) in nhds x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U

## 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.

## Equations

- H.EquicontinuousAt x₀ = EquicontinuousAt Subtype.val x₀

## Instances For

A family `F : ι → X → α`

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

`U ∈ 𝓤 α`

, there is a
neighborhood `V`

of `x₀`

within `S`

such that, for all `x ∈ V`

and for all `i : ι`

, `F i x`

is
`U`

-close to `F i x₀`

.## Equations

- EquicontinuousWithinAt F S x₀ = ∀ U ∈ uniformity α, ∀ᶠ (x : X) in nhdsWithin x₀ S, ∀ (i : ι), (F i x₀, F i x) ∈ U

## Instances For

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

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

is equicontinuous at that point within that same subset.

## Equations

- H.EquicontinuousWithinAt S x₀ = EquicontinuousWithinAt Subtype.val S x₀

## 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`

.

## Equations

- Equicontinuous F = ∀ (x₀ : X), EquicontinuousAt F x₀

## Instances For

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

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

is equicontinuous.

## Equations

- H.Equicontinuous = Equicontinuous Subtype.val

## Instances For

A family `F : ι → X → α`

of functions from a topological space to a uniform space is
*equicontinuous on S : Set X* if it is equicontinuous

*within*at each point of

`S`

`S`

.## Equations

- EquicontinuousOn F S = ∀ x₀ ∈ S, EquicontinuousWithinAt F S x₀

## Instances For

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

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

is equicontinuous on that subset.

## Equations

- H.EquicontinuousOn S = EquicontinuousOn Subtype.val S

## Instances For

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`

.## Equations

- UniformEquicontinuous F = ∀ U ∈ uniformity α, ∀ᶠ (xy : β × β) in uniformity β, ∀ (i : ι), (F i xy.1, F i xy.2) ∈ U

## Instances For

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

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

is uniformly equicontinuous.

## Equations

- H.UniformEquicontinuous = UniformEquicontinuous Subtype.val

## Instances For

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`

.## Equations

- UniformEquicontinuousOn F S = ∀ U ∈ uniformity α, ∀ᶠ (xy : β × β) in uniformity β ⊓ Filter.principal (S ×ˢ S), ∀ (i : ι), (F i xy.1, F i xy.2) ∈ U

## Instances For

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

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

is uniformly equicontinuous on that subset.

## Equations

- H.UniformEquicontinuousOn S = UniformEquicontinuousOn Subtype.val S

## Instances For

### Empty index type #

### Finite index type #

### Index type with a unique element #

Reformulation of equicontinuity at `x₀`

within a set `S`

, comparing two variables near `x₀`

instead of comparing only one with `x₀`

.

Reformulation of equicontinuity at `x₀`

comparing two variables near `x₀`

instead of comparing
only one with `x₀`

.

Uniform equicontinuity implies equicontinuity.

Uniform equicontinuity on a subset implies equicontinuity on that subset.

Each function of a family equicontinuous at `x₀`

is continuous at `x₀`

.

Each function of a family equicontinuous at `x₀`

within `S`

is continuous at `x₀`

within `S`

.

Each function of an equicontinuous family is continuous.

Each function of a family equicontinuous on `S`

is continuous on `S`

.

Each function of a uniformly equicontinuous family is uniformly continuous.

Each function of a family uniformly equicontinuous on `S`

is uniformly continuous on `S`

.

Taking sub-families preserves equicontinuity at a point.

Taking sub-families preserves equicontinuity at a point within a subset.

Taking sub-families preserves equicontinuity.

Taking sub-families preserves equicontinuity on a subset.

Taking sub-families preserves uniform equicontinuity.

Taking sub-families preserves uniform equicontinuity on a subset.

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 at `x₀`

within `S`

iff `range 𝓕`

is equicontinuous
at `x₀`

within `S`

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

is equicontinuous at `x₀`

within `S`

.

A family `𝓕 : ι → X → α`

is equicontinuous iff `range 𝓕`

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

is equicontinuous.

A family `𝓕 : ι → X → α`

is equicontinuous on `S`

iff `range 𝓕`

is equicontinuous on `S`

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

is equicontinuous on `S`

.

A family `𝓕 : ι → β → α`

is uniformly equicontinuous iff `range 𝓕`

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

is uniformly equicontinuous.

A family `𝓕 : ι → β → α`

is uniformly equicontinuous on `S`

iff `range 𝓕`

is uniformly
equicontinuous on `S`

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

is uniformly equicontinuous on `S`

.

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 developing the equicontinuity API, but it should not be used directly for other
purposes.

A family `𝓕 : ι → X → α`

is equicontinuous at `x₀`

within `S`

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

is continuous at `x₀`

within `S`

*when ι → α is equipped with the topology of uniform convergence*. This is very useful for
developing 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 developing the equicontinuity API, but it should not be used directly for other
purposes.

A family `𝓕 : ι → X → α`

is equicontinuous on `S`

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

is
continuous on `S`

*when ι → α is equipped with the topology of uniform convergence*. This is
very useful for developing 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 developing the equicontinuity API, but it should not be used directly
for other purposes.

A family `𝓕 : ι → β → α`

is uniformly equicontinuous on `S`

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

is uniformly continuous on `S`

*when ι → α is equipped with the uniform structure of uniform convergence*. This is very useful
for developing 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 composing each function of `𝓕`

by `u`

, is
equicontinuous at `x₀`

.

**Alias** of `IsUniformInducing.equicontinuousAt_iff`

.

Given `u : α → β`

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

is equicontinuous at a point
`x₀ : X`

iff the family `𝓕'`

, obtained by composing each function of `𝓕`

by `u`

, is
equicontinuous at `x₀`

.

Given `u : α → β`

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

is equicontinuous at a point
`x₀ : X`

within a subset `S : Set X`

iff the family `𝓕'`

, obtained by composing each function
of `𝓕`

by `u`

, is equicontinuous at `x₀`

within `S`

.

**Alias** of `IsUniformInducing.equicontinuousWithinAt_iff`

.

Given `u : α → β`

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

is equicontinuous at a point
`x₀ : X`

within a subset `S : Set X`

iff the family `𝓕'`

, obtained by composing each function
of `𝓕`

by `u`

, is equicontinuous at `x₀`

within `S`

.

Given `u : α → β`

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

is equicontinuous iff the
family `𝓕'`

, obtained by composing each function of `𝓕`

by `u`

, is equicontinuous.

**Alias** of `IsUniformInducing.equicontinuous_iff`

.

Given `u : α → β`

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

is equicontinuous iff the
family `𝓕'`

, obtained by composing each function of `𝓕`

by `u`

, is equicontinuous.

Given `u : α → β`

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

is equicontinuous on a
subset `S : Set X`

iff the family `𝓕'`

, obtained by composing each function of `𝓕`

by `u`

, is
equicontinuous on `S`

.

**Alias** of `IsUniformInducing.equicontinuousOn_iff`

.

Given `u : α → β`

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

is equicontinuous on a
subset `S : Set X`

iff the family `𝓕'`

, obtained by composing each function of `𝓕`

by `u`

, is
equicontinuous on `S`

.

Given `u : α → γ`

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

is uniformly equicontinuous
iff the family `𝓕'`

, obtained by composing each function of `𝓕`

by `u`

, is uniformly
equicontinuous.

**Alias** of `IsUniformInducing.uniformEquicontinuous_iff`

.

Given `u : α → γ`

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

is uniformly equicontinuous
iff the family `𝓕'`

, obtained by composing each function of `𝓕`

by `u`

, is uniformly
equicontinuous.

Given `u : α → γ`

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

is uniformly equicontinuous
on a subset `S : Set β`

iff the family `𝓕'`

, obtained by composing each function of `𝓕`

by `u`

,
is uniformly equicontinuous on `S`

.

**Alias** of `IsUniformInducing.uniformEquicontinuousOn_iff`

.

Given `u : α → γ`

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

is uniformly equicontinuous
on a subset `S : Set β`

iff the family `𝓕'`

, obtained by composing each function of `𝓕`

by `u`

,
is uniformly equicontinuous on `S`

.

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

within a set `S`

, the same is true for its
closure in *any* topology for which evaluation at any `x ∈ S ∪ {x₀}`

is continuous. Since
this will be applied to `DFunLike`

types, we state it for any topological space with a map
to `X → α`

satisfying the right continuity conditions. See also `Set.EquicontinuousWithinAt.closure`

for a more familiar (but weaker) statement.

Note: This could *technically* be called `EquicontinuousWithinAt.closure`

without name clashes
with `Set.EquicontinuousWithinAt.closure`

, but we don't do it because, even with a `protected`

marker, it would introduce ambiguities while working in namespace `Set`

(e.g, in the proof of
any theorem called `Set.something`

).

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

, the same is true for its closure in *any*
topology for which evaluation at any point is continuous. Since this will be applied to
`DFunLike`

types, we state it for any topological space with a map to `X → α`

satisfying the right
continuity conditions. See also `Set.EquicontinuousAt.closure`

for a more familiar statement.

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

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

.

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

within a set `S`

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

within `S`

. This would also be true for the coarser
topology of pointwise convergence on `S ∪ {x₀}`

, see `Set.EquicontinuousWithinAt.closure'`

.

If a set of functions is equicontinuous, the same is true for its closure in *any*
topology for which evaluation at any point is continuous. Since this will be applied to
`DFunLike`

types, we state it for any topological space with a map to `X → α`

satisfying the right
continuity conditions. See also `Set.Equicontinuous.closure`

for a more familiar statement.

If a set of functions is equicontinuous on a set `S`

, the same is true for its closure in *any*
topology for which evaluation at any `x ∈ S`

is continuous. Since this will be applied to
`DFunLike`

types, we state it for any topological space with a map to `X → α`

satisfying the right
continuity conditions. See also `Set.EquicontinuousOn.closure`

for a more familiar
(but weaker) statement.

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

If a set of functions is equicontinuous, its closure for the product topology is also
equicontinuous. This would also be true for the coarser topology of pointwise convergence on `S`

,
see `EquicontinuousOn.closure'`

.

If a set of functions is uniformly equicontinuous on a set `S`

, the same is true for its
closure in *any* topology for which evaluation at any `x ∈ S`

i continuous. Since this will be
applied to `DFunLike`

types, we state it for any topological space with a map to `β → α`

satisfying
the right continuity conditions. See also `Set.UniformEquicontinuousOn.closure`

for a more familiar
(but weaker) statement.

If a set of functions is uniformly equicontinuous, the same is true for its closure in *any*
topology for which evaluation at any point is continuous. Since this will be applied to
`DFunLike`

types, we state it for any topological space with a map to `β → α`

satisfying the right
continuity conditions. See also `Set.UniformEquicontinuous.closure`

for a more familiar statement.

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

If a set of functions is uniformly equicontinuous on a set `S`

, its closure for the product
topology is also uniformly equicontinuous. This would also be true for the coarser topology of
pointwise convergence on `S`

, see `UniformEquicontinuousOn.closure'`

.

If `𝓕 : ι → X → α`

tends to `f : X → α`

*pointwise on S ∪ {x₀} : Set X* along some nontrivial
filter, and if the family

`𝓕`

is equicontinuous at `x₀ : X`

within `S`

, then the limit is
continuous at `x₀`

within `S`

.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₀`

.

If `𝓕 : ι → X → α`

tends to `f : X → α`

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

is equicontinuous, then the limit is continuous.

If `𝓕 : ι → X → α`

tends to `f : X → α`

*pointwise on S : Set X* along some nontrivial
filter, and if the family

`𝓕`

is equicontinuous, then the limit is continuous on `S`

.If `𝓕 : ι → β → α`

tends to `f : β → α`

*pointwise on S : Set β* along some nontrivial
filter, and if the family

`𝓕`

is uniformly equicontinuous on `S`

, then the limit is uniformly
continuous on `S`

.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.