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.
A filter 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.
A set 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).
theorem
cauchy_map_iff
{α : Type u}
{β : Type v}
[uniform_space α]
{l : filter β}
{f : β → α} :
cauchy (filter.map f l) ↔ l.ne_bot ∧ filter.tendsto (λ (p : β × β), (f p.fst, f p.snd)) (l.prod l) (uniformity α)
theorem
cauchy_map_iff'
{α : Type u}
{β : Type v}
[uniform_space α]
{l : filter β}
[hl : l.ne_bot]
{f : β → α} :
cauchy (filter.map f l) ↔ filter.tendsto (λ (p : β × β), (f p.fst, f p.snd)) (l.prod l) (uniformity α)
theorem
cauchy.mono
{α : Type u}
[uniform_space α]
{f g : filter α}
[hg : g.ne_bot]
(h_c : cauchy f)
(h_le : g ≤ f) :
cauchy g
theorem
cauchy.mono'
{α : Type u}
[uniform_space α]
{f g : filter α}
(h_c : cauchy f)
(hg : g.ne_bot)
(h_le : g ≤ f) :
cauchy g
theorem
filter.tendsto.cauchy_map
{α : Type u}
{β : Type v}
[uniform_space α]
{l : filter β}
[l.ne_bot]
{f : β → α}
{a : α}
(h : filter.tendsto f l (nhds a)) :
cauchy (filter.map f l)
theorem
cauchy.prod
{α : Type u}
{β : Type v}
[uniform_space α]
[uniform_space β]
{f : filter α}
{g : filter β}
(hf : cauchy f)
(hg : cauchy g) :
theorem
le_nhds_of_cauchy_adhp_aux
{α : Type u}
[uniform_space α]
{f : filter α}
{x : α}
(adhs : ∀ (s : set (α × α)), s ∈ uniformity α → (∃ (t : set α) (H : t ∈ f), t ×ˢ t ⊆ s ∧ ∃ (y : α), (x, y) ∈ s ∧ y ∈ t)) :
The common part of the proofs of le_nhds_of_cauchy_adhp and
sequentially_complete.le_nhds_of_seq_tendsto_nhds: if for any entourage s
one can choose a set t ∈ f of diameter s such that it contains a point y
with (x, y) ∈ s, then f converges to x.
theorem
le_nhds_of_cauchy_adhp
{α : Type u}
[uniform_space α]
{f : filter α}
{x : α}
(hf : cauchy f)
(adhs : cluster_pt x f) :
If x is an adherent (cluster) point for a Cauchy filter f, then it is a limit point
for f.
theorem
le_nhds_iff_adhp_of_cauchy
{α : Type u}
[uniform_space α]
{f : filter α}
{x : α}
(hf : cauchy f) :
f ≤ nhds x ↔ cluster_pt x f
theorem
cauchy.map
{α : Type u}
{β : Type v}
[uniform_space α]
[uniform_space β]
{f : filter α}
{m : α → β}
(hf : cauchy f)
(hm : uniform_continuous m) :
cauchy (filter.map m f)
theorem
cauchy.comap
{α : Type u}
{β : Type v}
[uniform_space α]
[uniform_space β]
{f : filter β}
{m : α → β}
(hf : cauchy f)
(hm : filter.comap (λ (p : α × α), (m p.fst, m p.snd)) (uniformity β) ≤ uniformity α)
[(filter.comap m f).ne_bot] :
cauchy (filter.comap m f)
theorem
cauchy.comap'
{α : Type u}
{β : Type v}
[uniform_space α]
[uniform_space β]
{f : filter β}
{m : α → β}
(hf : cauchy f)
(hm : filter.comap (λ (p : α × α), (m p.fst, m p.snd)) (uniformity β) ≤ uniformity α)
(hb : (filter.comap m f).ne_bot) :
cauchy (filter.comap m f)
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.
Equations
- cauchy_seq u = cauchy (filter.map u filter.at_top)
theorem
cauchy_seq.tendsto_uniformity
{α : Type u}
{β : Type v}
[uniform_space α]
[semilattice_sup β]
{u : β → α}
(h : cauchy_seq u) :
filter.tendsto (prod.map u u) filter.at_top (uniformity α)
theorem
cauchy_seq.nonempty
{α : Type u}
{β : Type v}
[uniform_space α]
[semilattice_sup β]
{u : β → α}
(hu : cauchy_seq u) :
nonempty β
theorem
cauchy_seq.mem_entourage
{α : Type u}
[uniform_space α]
{β : Type u_1}
[semilattice_sup β]
{u : β → α}
(h : cauchy_seq u)
{V : set (α × α)}
(hV : V ∈ uniformity α) :
theorem
filter.tendsto.cauchy_seq
{α : Type u}
{β : Type v}
[uniform_space α]
[semilattice_sup β]
[nonempty β]
{f : β → α}
{x : α}
(hx : filter.tendsto f filter.at_top (nhds x)) :
theorem
cauchy_seq_const
{α : Type u}
{β : Type v}
[uniform_space α]
[semilattice_sup β]
[nonempty β]
(x : α) :
cauchy_seq (λ (n : β), x)
theorem
cauchy_seq_iff_tendsto
{α : Type u}
{β : Type v}
[uniform_space α]
[nonempty β]
[semilattice_sup β]
{u : β → α} :
cauchy_seq u ↔ filter.tendsto (prod.map u u) filter.at_top (uniformity α)
theorem
cauchy_seq.comp_tendsto
{α : Type u}
{β : Type v}
[uniform_space α]
{γ : Type u_1}
[semilattice_sup β]
[semilattice_sup γ]
[nonempty γ]
{f : β → α}
(hf : cauchy_seq f)
{g : γ → β}
(hg : filter.tendsto g filter.at_top filter.at_top) :
cauchy_seq (f ∘ g)
theorem
cauchy_seq.comp_injective
{α : Type u}
{β : Type v}
[uniform_space α]
[semilattice_sup β]
[no_max_order β]
[nonempty β]
{u : ℕ → α}
(hu : cauchy_seq u)
{f : β → ℕ}
(hf : function.injective f) :
cauchy_seq (u ∘ f)
theorem
function.bijective.cauchy_seq_comp_iff
{α : Type u}
[uniform_space α]
{f : ℕ → ℕ}
(hf : function.bijective f)
(u : ℕ → α) :
cauchy_seq (u ∘ f) ↔ cauchy_seq u
theorem
cauchy_seq.subseq_subseq_mem
{α : Type u}
[uniform_space α]
{V : ℕ → set (α × α)}
(hV : ∀ (n : ℕ), V n ∈ uniformity α)
{u : ℕ → α}
(hu : cauchy_seq u)
{f g : ℕ → ℕ}
(hf : filter.tendsto f filter.at_top filter.at_top)
(hg : filter.tendsto g filter.at_top filter.at_top) :
theorem
cauchy_seq.prod_map
{α : Type u}
{β : Type v}
[uniform_space α]
{γ : Type u_1}
{δ : Type u_2}
[uniform_space β]
[semilattice_sup γ]
[semilattice_sup δ]
{u : γ → α}
{v : δ → β}
(hu : cauchy_seq u)
(hv : cauchy_seq v) :
cauchy_seq (prod.map u v)
theorem
cauchy_seq.prod
{α : Type u}
{β : Type v}
[uniform_space α]
{γ : Type u_1}
[uniform_space β]
[semilattice_sup γ]
{u : γ → α}
{v : γ → β}
(hu : cauchy_seq u)
(hv : cauchy_seq v) :
cauchy_seq (λ (x : γ), (u x, v x))
theorem
cauchy_seq.eventually_eventually
{α : Type u}
{β : Type v}
[uniform_space α]
[semilattice_sup β]
{u : β → α}
(hu : cauchy_seq u)
{V : set (α × α)}
(hV : V ∈ uniformity α) :
∀ᶠ (k : β) in filter.at_top, ∀ᶠ (l : β) in filter.at_top, (u k, u l) ∈ V
theorem
uniform_continuous.comp_cauchy_seq
{α : Type u}
{β : Type v}
[uniform_space α]
{γ : Type u_1}
[uniform_space β]
[semilattice_sup γ]
{f : α → β}
(hf : uniform_continuous f)
{u : γ → α}
(hu : cauchy_seq u) :
cauchy_seq (f ∘ u)
theorem
filter.tendsto.subseq_mem_entourage
{α : Type u}
[uniform_space α]
{V : ℕ → set (α × α)}
(hV : ∀ (n : ℕ), V n ∈ uniformity α)
{u : ℕ → α}
{a : α}
(hu : filter.tendsto u filter.at_top (nhds a)) :
theorem
tendsto_nhds_of_cauchy_seq_of_subseq
{α : Type u}
{β : Type v}
[uniform_space α]
[semilattice_sup β]
{u : β → α}
(hu : cauchy_seq u)
{ι : Type u_1}
{f : ι → β}
{p : filter ι}
[p.ne_bot]
(hf : filter.tendsto f p filter.at_top)
{a : α}
(ha : filter.tendsto (u ∘ f) p (nhds a)) :
filter.tendsto u filter.at_top (nhds a)
If a Cauchy sequence has a convergent subsequence, then it converges.
@[nolint]
theorem
filter.has_basis.cauchy_seq_iff
{α : Type u}
{β : Type v}
[uniform_space α]
{γ : Sort u_1}
[nonempty β]
[semilattice_sup β]
{u : β → α}
{p : γ → Prop}
{s : γ → set (α × α)}
(h : (uniformity α).has_basis p s) :
theorem
filter.has_basis.cauchy_seq_iff'
{α : Type u}
{β : Type v}
[uniform_space α]
{γ : Sort u_1}
[nonempty β]
[semilattice_sup β]
{u : β → α}
{p : γ → Prop}
{s : γ → set (α × α)}
(H : (uniformity α).has_basis p s) :
theorem
is_complete_iff_cluster_pt
{α : Type u}
[uniform_space α]
{s : set α} :
is_complete s ↔ ∀ (l : filter α), cauchy l → l ≤ filter.principal s → (∃ (x : α) (H : x ∈ s), cluster_pt x l)
@[protected]
theorem
is_complete.union
{α : Type u}
[uniform_space α]
{s t : set α}
(hs : is_complete s)
(ht : is_complete t) :
is_complete (s ∪ t)
theorem
is_complete_Union_separated
{α : Type u}
[uniform_space α]
{ι : Sort u_1}
{s : ι → set α}
(hs : ∀ (i : ι), is_complete (s i))
{U : set (α × α)}
(hU : U ∈ uniformity α)
(hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j) :
is_complete (⋃ (i : ι), s i)
@[class]
A complete space is defined here using uniformities. A uniform space is complete if every Cauchy filter converges.
Instances of this typeclass
- complete_of_compact
- complete_of_proper
- continuous_linear_map.complete_space_ker
- is_R_or_C.to_complete_space
- complete_space.prod
- complete_space.mul_opposite
- complete_space.add_opposite
- ulift.complete_space
- complete_space.sum
- Pi.complete
- quotient_group.complete_space'
- quotient_add_group.complete_space'
- quotient_group.complete_space
- quotient_add_group.complete_space
- Cauchy.complete_space
- uniform_space.complete_space_separation
- uniform_space.completion.complete_space
- real.complete_space
- submodule.topological_closure.complete_space
- linear_isometry.complete_space_map
- linear_isometry.complete_space_map'
- linear_isometry_equiv.complete_space_map
- star_subalgebra.topological_closure.complete_space
- elemental_star_algebra.complete_space
- complex.complete_space
- continuous_linear_map.complete_space
- continuous_multilinear_map.complete_space
@[protected, instance]
def
complete_space.prod
{α : Type u}
{β : Type v}
[uniform_space α]
[uniform_space β]
[complete_space α]
[complete_space β] :
complete_space (α × β)
@[protected, instance]
@[protected, instance]
theorem
complete_space_of_is_complete_univ
{α : Type u}
[uniform_space α]
(h : is_complete set.univ) :
If univ is complete, the space is a complete space
theorem
cauchy_iff_exists_le_nhds
{α : Type u}
[uniform_space α]
[complete_space α]
{l : filter α}
[l.ne_bot] :
theorem
cauchy_map_iff_exists_tendsto
{α : Type u}
{β : Type v}
[uniform_space α]
[complete_space α]
{l : filter β}
{f : β → α}
[l.ne_bot] :
cauchy (filter.map f l) ↔ ∃ (x : α), filter.tendsto f l (nhds x)
theorem
cauchy_seq_tendsto_of_complete
{α : Type u}
{β : Type v}
[uniform_space α]
[semilattice_sup β]
[complete_space α]
{u : β → α}
(H : cauchy_seq u) :
∃ (x : α), filter.tendsto u filter.at_top (nhds x)
A Cauchy sequence in a complete space converges
theorem
cauchy_seq_tendsto_of_is_complete
{α : Type u}
{β : Type v}
[uniform_space α]
[semilattice_sup β]
{K : set α}
(h₁ : is_complete K)
{u : β → α}
(h₂ : ∀ (n : β), u n ∈ K)
(h₃ : cauchy_seq u) :
∃ (v : α) (H : v ∈ K), filter.tendsto u filter.at_top (nhds v)
If K is a complete subset, then any cauchy sequence in K converges to a point in K
theorem
cauchy.le_nhds_Lim
{α : Type u}
[uniform_space α]
[complete_space α]
[nonempty α]
{f : filter α}
(hf : cauchy f) :
theorem
cauchy_seq.tendsto_lim
{α : Type u}
{β : Type v}
[uniform_space α]
[semilattice_sup β]
[complete_space α]
[nonempty α]
{u : β → α}
(h : cauchy_seq u) :
filter.tendsto u filter.at_top (nhds (lim filter.at_top u))
theorem
is_closed.is_complete
{α : Type u}
[uniform_space α]
[complete_space α]
{s : set α}
(h : is_closed s) :
A set s is totally bounded if for every entourage d there is a finite
set of points t such that every element of s is d-near to some element of t.
theorem
totally_bounded_of_forall_symm
{α : Type u}
[uniform_space α]
{s : set α}
(h : ∀ (V : set (α × α)), V ∈ uniformity α → symmetric_rel V → (∃ (t : set α), t.finite ∧ s ⊆ ⋃ (y : α) (H : y ∈ t), uniform_space.ball y V)) :
theorem
totally_bounded_subset
{α : Type u}
[uniform_space α]
{s₁ s₂ : set α}
(hs : s₁ ⊆ s₂)
(h : totally_bounded s₂) :
theorem
totally_bounded.closure
{α : Type u}
[uniform_space α]
{s : set α}
(h : totally_bounded s) :
The closure of a totally bounded set is totally bounded.
theorem
totally_bounded.image
{α : Type u}
{β : Type v}
[uniform_space α]
[uniform_space β]
{f : α → β}
{s : set α}
(hs : totally_bounded s)
(hf : uniform_continuous f) :
totally_bounded (f '' s)
The image of a totally bounded set under a uniformly continuous map is totally bounded.
theorem
ultrafilter.cauchy_of_totally_bounded
{α : Type u}
[uniform_space α]
{s : set α}
(f : ultrafilter α)
(hs : totally_bounded s)
(h : ↑f ≤ filter.principal s) :
theorem
totally_bounded_iff_ultrafilter
{α : Type u}
[uniform_space α]
{s : set α} :
totally_bounded s ↔ ∀ (f : ultrafilter α), ↑f ≤ filter.principal s → cauchy ↑f
theorem
is_compact_iff_totally_bounded_is_complete
{α : Type u}
[uniform_space α]
{s : set α} :
is_compact s ↔ totally_bounded s ∧ is_complete s
@[protected]
@[protected]
@[protected, instance]
theorem
is_compact_of_totally_bounded_is_closed
{α : Type u}
[uniform_space α]
[complete_space α]
{s : set α}
(ht : totally_bounded s)
(hc : is_closed s) :
theorem
cauchy_seq.totally_bounded_range
{α : Type u}
[uniform_space α]
{s : ℕ → α}
(hs : cauchy_seq s) :
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 topology/metric_space/emetric_space
and topology/metric_space/basic.
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
sets 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 a, then f ≤ 𝓝 a.
noncomputable
def
sequentially_complete.set_seq_aux
{α : Type u}
[uniform_space α]
{f : filter α}
(hf : cauchy f)
{U : ℕ → set (α × α)}
(U_mem : ∀ (n : ℕ), U n ∈ uniformity α)
(n : ℕ) :
An auxiliary sequence of sets approximating a Cauchy filter.
Equations
- sequentially_complete.set_seq_aux hf U_mem n = classical.indefinite_description (λ (s : set α), ∃ (_x : s ∈ f), s ×ˢ s ⊆ U n) _
def
sequentially_complete.set_seq
{α : Type u}
[uniform_space α]
{f : filter α}
(hf : cauchy f)
{U : ℕ → set (α × α)}
(U_mem : ∀ (n : ℕ), U n ∈ uniformity α)
(n : ℕ) :
set α
Given a Cauchy filter f and a sequence U of entourages, set_seq provides
an antitone sequence of sets s n ∈ f such that s n ×ˢ s n ⊆ U.
Equations
- sequentially_complete.set_seq hf U_mem n = ⋂ (m : ℕ) (H : m ∈ set.Iic n), (sequentially_complete.set_seq_aux hf U_mem m).val
theorem
sequentially_complete.set_seq_mem
{α : Type u}
[uniform_space α]
{f : filter α}
(hf : cauchy f)
{U : ℕ → set (α × α)}
(U_mem : ∀ (n : ℕ), U n ∈ uniformity α)
(n : ℕ) :
sequentially_complete.set_seq hf U_mem n ∈ f
theorem
sequentially_complete.set_seq_mono
{α : Type u}
[uniform_space α]
{f : filter α}
(hf : cauchy f)
{U : ℕ → set (α × α)}
(U_mem : ∀ (n : ℕ), U n ∈ uniformity α)
⦃m n : ℕ⦄
(h : m ≤ n) :
sequentially_complete.set_seq hf U_mem n ⊆ sequentially_complete.set_seq hf U_mem m
theorem
sequentially_complete.set_seq_sub_aux
{α : Type u}
[uniform_space α]
{f : filter α}
(hf : cauchy f)
{U : ℕ → set (α × α)}
(U_mem : ∀ (n : ℕ), U n ∈ uniformity α)
(n : ℕ) :
sequentially_complete.set_seq hf U_mem n ⊆ ↑(sequentially_complete.set_seq_aux hf U_mem n)
theorem
sequentially_complete.set_seq_prod_subset
{α : Type u}
[uniform_space α]
{f : filter α}
(hf : cauchy f)
{U : ℕ → set (α × α)}
(U_mem : ∀ (n : ℕ), U n ∈ uniformity α)
{N m n : ℕ}
(hm : N ≤ m)
(hn : N ≤ n) :
sequentially_complete.set_seq hf U_mem m ×ˢ sequentially_complete.set_seq hf U_mem n ⊆ U N
noncomputable
def
sequentially_complete.seq
{α : Type u}
[uniform_space α]
{f : filter α}
(hf : cauchy f)
{U : ℕ → set (α × α)}
(U_mem : ∀ (n : ℕ), U n ∈ uniformity α)
(n : ℕ) :
α
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
of entourages.
Equations
- sequentially_complete.seq hf U_mem n = classical.some _
theorem
sequentially_complete.seq_mem
{α : Type u}
[uniform_space α]
{f : filter α}
(hf : cauchy f)
{U : ℕ → set (α × α)}
(U_mem : ∀ (n : ℕ), U n ∈ uniformity α)
(n : ℕ) :
sequentially_complete.seq hf U_mem n ∈ sequentially_complete.set_seq hf U_mem n
theorem
sequentially_complete.seq_pair_mem
{α : Type u}
[uniform_space α]
{f : filter α}
(hf : cauchy f)
{U : ℕ → set (α × α)}
(U_mem : ∀ (n : ℕ), U n ∈ uniformity α)
⦃N m n : ℕ⦄
(hm : N ≤ m)
(hn : N ≤ n) :
(sequentially_complete.seq hf U_mem m, sequentially_complete.seq hf U_mem n) ∈ U N
theorem
sequentially_complete.seq_is_cauchy_seq
{α : Type u}
[uniform_space α]
{f : filter α}
(hf : cauchy f)
{U : ℕ → set (α × α)}
(U_mem : ∀ (n : ℕ), U n ∈ uniformity α)
(U_le : ∀ (s : set (α × α)), s ∈ uniformity α → (∃ (n : ℕ), U n ⊆ s)) :
cauchy_seq (sequentially_complete.seq hf U_mem)
theorem
sequentially_complete.le_nhds_of_seq_tendsto_nhds
{α : Type u}
[uniform_space α]
{f : filter α}
(hf : cauchy f)
{U : ℕ → set (α × α)}
(U_mem : ∀ (n : ℕ), U n ∈ uniformity α)
(U_le : ∀ (s : set (α × α)), s ∈ uniformity α → (∃ (n : ℕ), U n ⊆ s))
⦃a : α⦄
(ha : filter.tendsto (sequentially_complete.seq hf U_mem) filter.at_top (nhds a)) :
If the sequence sequentially_complete.seq converges to a, then f ≤ 𝓝 a.
theorem
uniform_space.complete_of_convergent_controlled_sequences
{α : Type u}
[uniform_space α]
[(uniformity α).is_countably_generated]
(U : ℕ → set (α × α))
(U_mem : ∀ (n : ℕ), U n ∈ uniformity α)
(HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → (∃ (a : α), filter.tendsto u filter.at_top (nhds 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.
theorem
uniform_space.complete_of_cauchy_seq_tendsto
{α : Type u}
[uniform_space α]
[(uniformity α).is_countably_generated]
(H' : ∀ (u : ℕ → α), cauchy_seq u → (∃ (a : α), filter.tendsto u filter.at_top (nhds a))) :
A sequentially complete uniform space with a countable basis of the uniformity filter is complete.
@[protected, instance]
theorem
uniform_space.second_countable_of_separable
(α : Type u)
[uniform_space α]
[(uniformity α).is_countably_generated]
[topological_space.separable_space α] :
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.