mathlib3 documentation

topology.uniform_space.cauchy

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.

def cauchy {α : Type u} [uniform_space α] (f : filter α) :
Prop

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.

Equations
def is_complete {α : Type u} [uniform_space α] (s : set α) :
Prop

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

Equations
theorem filter.has_basis.cauchy_iff {α : Type u} [uniform_space α] {ι : Sort u_1} {p : ι Prop} {s : ι set × α)} (h : (uniformity α).has_basis p s) {f : filter α} :
cauchy f f.ne_bot (i : ι), p i ( (t : set α) (H : t f), (x : α), x t (y : α), y t (x, y) s i)
theorem cauchy_iff' {α : Type u} [uniform_space α] {f : filter α} :
cauchy f f.ne_bot (s : set × α)), s uniformity α ( (t : set α) (H : t f), (x : α), x t (y : α), y t (x, y) s)
theorem cauchy_iff {α : Type u} [uniform_space α] {f : filter α} :
cauchy f f.ne_bot (s : set × α)), s uniformity α ( (t : set α) (H : t f), t ×ˢ t s)
theorem cauchy.ultrafilter_of {α : Type u} [uniform_space α] {l : filter α} (h : cauchy l) :
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) :
theorem cauchy.mono' {α : Type u} [uniform_space α] {f g : filter α} (h_c : cauchy f) (hg : g.ne_bot) (h_le : g f) :
theorem cauchy_nhds {α : Type u} [uniform_space α] {a : α} :
theorem cauchy_pure {α : Type u} [uniform_space α] {a : α} :
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)) :
theorem cauchy.prod {α : Type u} {β : Type v} [uniform_space α] [uniform_space β] {f : filter α} {g : filter β} (hf : cauchy f) (hg : cauchy g) :
cauchy (f.prod 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)) :
f nhds x

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) :
f nhds x

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) :
theorem cauchy.map {α : Type u} {β : Type v} [uniform_space α] [uniform_space β] {f : filter α} {m : α β} (hf : cauchy f) (hm : uniform_continuous m) :
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] :
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) :
def cauchy_seq {α : Type u} {β : Type v} [uniform_space α] [semilattice_sup β] (u : β α) :
Prop

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
theorem cauchy_seq.nonempty {α : Type u} {β : Type v} [uniform_space α] [semilattice_sup β] {u : β α} (hu : cauchy_seq u) :
theorem cauchy_seq.mem_entourage {α : Type u} [uniform_space α] {β : Type u_1} [semilattice_sup β] {u : β α} (h : cauchy_seq u) {V : set × α)} (hV : V uniformity α) :
(k₀ : β), (i j : β), k₀ i k₀ j (u i, u j) V
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.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) :
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) :
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) :
(φ : ), strict_mono φ (n : ), ((u f φ) n, (u g φ) n) V n
theorem cauchy_seq_iff' {α : Type u} [uniform_space α] {u : α} :
theorem cauchy_seq_iff {α : Type u} [uniform_space α] {u : α} :
cauchy_seq u (V : set × α)), V uniformity α ( (N : ), (k : ), k N (l : ), l N (u k, u l) V)
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) :
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) :
theorem cauchy_seq.subseq_mem {α : Type u} [uniform_space α] {V : set × α)} (hV : (n : ), V n uniformity α) {u : α} (hu : cauchy_seq u) :
(φ : ), strict_mono φ (n : ), (u (n + 1)), u (φ n)) V n
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)) :
(φ : ), strict_mono φ (u (φ 0), a) V 0 (n : ), (u (n + 1)), u (φ n)) V (n + 1)
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)) :

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) :
cauchy_seq u (i : γ), p i ( (N : β), (m : β), m N (n : β), n N (u m, u n) s i)
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) :
cauchy_seq u (i : γ), p i ( (N : β), (n : β), n N (u n, u N) s i)
theorem cauchy_seq_of_controlled {α : Type u} {β : Type v} [uniform_space α] [semilattice_sup β] [nonempty β] (U : β set × α)) (hU : (s : set × α)), s uniformity α ( (n : β), U n s)) {f : β α} (hf : {N m n : β}, N m N n (f m, f n) U N) :
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)
theorem is_complete_iff_ultrafilter {α : Type u} [uniform_space α] {s : set α} :
is_complete s (l : ultrafilter α), cauchy l l filter.principal s ( (x : α) (H : x s), l nhds x)
theorem is_complete_iff_ultrafilter' {α : Type u} [uniform_space α] {s : set α} :
is_complete s (l : ultrafilter α), cauchy l s l ( (x : α) (H : x s), l nhds x)
@[protected]
theorem is_complete.union {α : Type u} [uniform_space α] {s t : set α} (hs : is_complete s) (ht : is_complete 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)
@[protected, instance]
@[protected, instance]
@[protected, instance]

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] :
cauchy l (x : α), l nhds x
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) :

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) :
f nhds (Lim f)
theorem is_closed.is_complete {α : Type u} [uniform_space α] [complete_space α] {s : set α} (h : is_closed s) :
def totally_bounded {α : Type u} [uniform_space α] (s : set α) :
Prop

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.

Equations
theorem totally_bounded.exists_subset {α : Type u} [uniform_space α] {s : set α} (hs : totally_bounded s) {U : set × α)} (hU : U uniformity α) :
(t : set α) (H : t s), t.finite s (y : α) (H : y t), {x : α | (x, y) U}
theorem totally_bounded_iff_subset {α : Type u} [uniform_space α] {s : set α} :
totally_bounded s (d : set × α)), d uniformity α ( (t : set α) (H : t s), t.finite s (y : α) (H : y t), {x : α | (x, y) d})
theorem filter.has_basis.totally_bounded_iff {α : Type u} [uniform_space α] {ι : Sort u_1} {p : ι Prop} {U : ι set × α)} (H : (uniformity α).has_basis p U) {s : set α} :
totally_bounded s (i : ι), p i ( (t : set α), t.finite s (y : α) (H : y t), {x : α | (x, y) U i})
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) :

The image of a totally bounded set under a uniformly continuous map is totally bounded.

theorem totally_bounded_iff_filter {α : Type u} [uniform_space α] {s : set α} :
totally_bounded s (f : filter α), f.ne_bot f filter.principal s ( (c : filter α) (H : c f), cauchy c)
@[protected]
theorem is_compact.totally_bounded {α : Type u} [uniform_space α] {s : set α} (h : is_compact s) :
@[protected]
theorem is_compact.is_complete {α : Type u} [uniform_space α] {s : set α} (h : is_compact s) :
@[protected, instance]

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 : ) :
{s // (_x : s f), s ×ˢ s U n}

An auxiliary sequence of sets approximating a Cauchy filter.

Equations
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
theorem sequentially_complete.set_seq_mem {α : Type u} [uniform_space α] {f : filter α} (hf : cauchy f) {U : set × α)} (U_mem : (n : ), U n uniformity α) (n : ) :
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) :
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 : ) :
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) :
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
theorem sequentially_complete.seq_mem {α : Type u} [uniform_space α] {f : filter α} (hf : cauchy f) {U : set × α)} (U_mem : (n : ), U n uniformity α) (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) :
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)) :
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)) :
f 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.

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.