Theory of Cauchy filters in uniform spaces. Complete uniform spaces. Totally bounded subsets. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
f is Cauchy if for every entourage
r, there exists an
s ∈ f such that
s × s ⊆ r. This is a generalization of Cauchy
sequences, because if
a : ℕ → α then the filter of sets containing
cofinitely many of the
a n is Cauchy iff
a is a Cauchy sequence.
s is called complete, if any Cauchy filter
f such that
s ∈ f
has a limit in
s (formally, it satisfies
f ≤ 𝓝 x for some
x ∈ s).
The common part of the proofs of
sequentially_complete.le_nhds_of_seq_tendsto_nhds: if for any entourage
one can choose a set
t ∈ f of diameter
s such that it contains a point
(x, y) ∈ s, then
f converges to
x is an adherent (cluster) point for a Cauchy filter
f, then it is a limit point
Cauchy sequences. Usually defined on ℕ, but often it is also useful to say that a function defined on ℝ is Cauchy at +∞ to deduce convergence. Therefore, we define it in a type class that is general enough to cover both ℕ and ℝ, which are the main motivating examples.
- cauchy_seq u = cauchy (filter.map u filter.at_top)
If a Cauchy sequence has a convergent subsequence, then it converges.
A complete space is defined here using uniformities. A uniform space is complete if every Cauchy filter converges.
Instances of this typeclass
univ is complete, the space is a complete space
A Cauchy sequence in a complete space converges
K is a complete subset, then any cauchy sequence in
K converges to a point in
s is totally bounded if for every entourage
d there is a finite
set of points
t such that every element of
d-near to some element of
The closure of a totally bounded set is totally bounded.
The image of a totally bounded set under a uniformly continuous map is totally bounded.
Every Cauchy sequence over
ℕ is totally bounded.
Sequentially complete space #
In this section we prove that a uniform space is complete provided that it is sequentially complete
(i.e., any Cauchy sequence converges) and its uniformity filter admits a countable generating set.
In particular, this applies to (e)metric spaces, see the files
More precisely, we assume that there is a sequence of entourages
U_n such that any other
entourage includes one of
U_n. Then any Cauchy filter
f generates a decreasing sequence of
s_n ∈ f such that
s_n × s_n ⊆ U_n. Choose a sequence
x_n∈s_n. It is easy to show
that this is a Cauchy sequence. If this sequence converges to some
f ≤ 𝓝 a.
An auxiliary sequence of sets approximating a Cauchy filter.
- sequentially_complete.set_seq_aux hf U_mem n = classical.indefinite_description (λ (s : set α), ∃ (_x : s ∈ f), s ×ˢ s ⊆ U n) _
Given a Cauchy filter
f and a sequence
U of entourages,
an antitone sequence of sets
s n ∈ f such that
s n ×ˢ s n ⊆ U.
- sequentially_complete.set_seq hf U_mem n = ⋂ (m : ℕ) (H : m ∈ set.Iic n), (sequentially_complete.set_seq_aux hf U_mem m).val
A sequence of points such that
seq n ∈ set_seq n. Here
set_seq is an antitone
sequence of sets
set_seq n ∈ f with diameters controlled by a given sequence
- sequentially_complete.seq hf U_mem n = classical.some _
If the sequence
sequentially_complete.seq converges to
f ≤ 𝓝 a.
A uniform space is complete provided that (a) its uniformity filter has a countable basis; (b) any sequence satisfying a "controlled" version of the Cauchy condition converges.
A sequentially complete uniform space with a countable basis of the uniformity filter is complete.
A separable uniform space with countably generated uniformity filter is second countable:
one obtains a countable basis by taking the balls centered at points in a dense subset,
and with rational "radii" from a countable open symmetric antitone basis of
𝓤 α. We do not
register this as an instance, as there is already an instance going in the other direction
from second countable spaces to separable spaces, and we want to avoid loops.