Equicontinuity of a family of functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Let X be a topological space and α a uniform_space. 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 #
equicontinuous_at: equicontinuity of a family of functions at a pointequicontinuous: equicontinuity of a family of functions on the whole domainuniform_equicontinuous: 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 typesX,Y,Zfor 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 familycoe : ↥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 setH : set homwould then have to be expressed as equicontinuity ofcoe_fn '' H, which is super annoying to work with. This is much simpler with families, because equicontinuity of a family𝓕 : ι → homwould simply be expressed as equicontinuity ofcoe_fn ∘ 𝓕, which doesn't introduce any nasty existentials.
To simplify statements, we do provide abbreviations set.equicontinuous_at, set.equicontinuous
and set.uniform_equicontinuous asserting the corresponding fact about the family
coe : ↥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 equicontinuous_within_at or equicontinuous_on), 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 #
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₀.
We say that a set H : set (X → α) of functions is equicontinuous at a point if the family
coe : ↥H → (X → α) is equicontinuous at that point.
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), equicontinuous_at F x₀
We say that a set H : set (X → α) of functions is equicontinuous if the family
coe : ↥H → (X → α) is equicontinuous.
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₀.
We say that a set H : set (X → α) of functions is uniformly equicontinuous if the family
coe : ↥H → (X → α) is uniformly equicontinuous.
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 coe : range F → X → α is equicontinuous at x₀.
A family 𝓕 : ι → X → α is equicontinuous iff range 𝓕 is equicontinuous,
i.e the family coe : range F → X → α is equicontinuous.
A family 𝓕 : ι → β → α is uniformly equicontinuous iff range 𝓕 is uniformly equicontinuous,
i.e the family coe : 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 equicontinuous_at.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 fun_like 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 fun_like 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 uniform_equicontinuous.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 fun_like 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.