# mathlibdocumentation

topology.uniform_space.cauchy

# Theory of Cauchy filters in uniform spaces. Complete uniform spaces. Totally bounded subsets. #

def cauchy {α : Type u} (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} (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} {β : Type v} {p : β → Prop} {s : β → set × α)} (h : (𝓤 α).has_basis p s) {f : filter α} :
f.ne_bot ∀ (i : β), p i(∃ (t : set α) (H : t f), ∀ (x y : α), x ty t(x, y) s i)
theorem cauchy_iff' {α : Type u} {f : filter α} :
f.ne_bot ∀ (s : set × α)), s 𝓤 α(∃ (t : set α) (H : t f), ∀ (x y : α), x ty t(x, y) s)
theorem cauchy_iff {α : Type u} {f : filter α} :
f.ne_bot ∀ (s : set × α)), s 𝓤 α(∃ (t : set α) (H : t f), t.prod t s)
theorem cauchy_map_iff {α : Type u} {β : Type v} {l : filter β} {f : β → α} :
cauchy l) l.ne_bot filter.tendsto (λ (p : β × β), (f p.fst, f p.snd)) (l ×ᶠ l) (𝓤 α)
theorem cauchy_map_iff' {α : Type u} {β : Type v} {l : filter β} [hl : l.ne_bot] {f : β → α} :
cauchy l) filter.tendsto (λ (p : β × β), (f p.fst, f p.snd)) (l ×ᶠ l) (𝓤 α)
theorem cauchy.mono {α : Type u} {f g : filter α} [hg : g.ne_bot] (h_c : cauchy f) (h_le : g f) :
theorem cauchy.mono' {α : Type u} {f g : filter α} (h_c : cauchy f) (hg : g.ne_bot) (h_le : g f) :
theorem cauchy_nhds {α : Type u} {a : α} :
theorem cauchy_pure {α : Type u} {a : α} :
theorem filter.tendsto.cauchy_map {α : Type u} {β : Type v} {l : filter β} [l.ne_bot] {f : β → α} {a : α} (h : (𝓝 a)) :
theorem le_nhds_of_cauchy_adhp_aux {α : Type u} {f : filter α} {x : α} (adhs : ∀ (s : set × α)), s 𝓤 α(∃ (t : set α) (H : t f), t.prod t s ∃ (y : α), (x, y) s y t)) :
f 𝓝 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} {f : filter α} {x : α} (hf : cauchy f) (adhs : f) :
f 𝓝 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} {f : filter α} {x : α} (hf : cauchy f) :
f 𝓝 x f
theorem cauchy.map {α : Type u} {β : Type v} {f : filter α} {m : α → β} (hf : cauchy f) (hm : uniform_continuous m) :
theorem cauchy.comap {α : Type u} {β : Type v} {f : filter β} {m : α → β} (hf : cauchy f) (hm : filter.comap (λ (p : α × α), (m p.fst, m p.snd)) (𝓤 β) 𝓤 α) [ f).ne_bot] :
theorem cauchy.comap' {α : Type u} {β : Type v} {f : filter β} {m : α → β} (hf : cauchy f) (hm : filter.comap (λ (p : α × α), (m p.fst, m p.snd)) (𝓤 β) 𝓤 α) (hb : f).ne_bot) :
def cauchy_seq {α : Type u} {β : Type v} (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.mem_entourage {α : Type u} {ι : Type u_1} [nonempty ι] [linear_order ι] {u : ι → α} (h : cauchy_seq u) {V : set × α)} (hV : V 𝓤 α) :
∃ (k₀ : ι), ∀ (i j : ι), k₀ ik₀ j(u i, u j) V
theorem filter.tendsto.cauchy_seq {α : Type u} {β : Type v} [nonempty β] {f : β → α} {x : α} (hx : (𝓝 x)) :
theorem cauchy_seq_const {α : Type u} (x : α) :
cauchy_seq (λ (n : ), x)
theorem cauchy_seq_iff_tendsto {α : Type u} {β : Type v} [nonempty β] {u : β → α} :
(𝓤 α)
theorem cauchy_seq.subseq_subseq_mem {α : Type u} {V : set × α)} (hV : ∀ (n : ), V n 𝓤 α) {u : → α} (hu : cauchy_seq u) {f g : }  :
∃ (φ : ), ∀ (n : ), ((u f φ) n, (u g φ) n) V n
theorem cauchy_seq_iff' {α : Type u} {u : → α} :
∀ (V : set × α)), V 𝓤 α(∀ᶠ (k : × ) in filter.at_top, k u ⁻¹' V)
theorem cauchy_seq_iff {α : Type u} {u : → α} :
∀ (V : set × α)), V 𝓤 α(∃ (N : ), ∀ (k : ), k N∀ (l : ), l N(u k, u l) V)
theorem cauchy_seq.subseq_mem {α : Type u} {V : set × α)} (hV : ∀ (n : ), V n 𝓤 α) {u : → α} (hu : cauchy_seq u) :
∃ (φ : ), ∀ (n : ), (u (n + 1)), u (φ n)) V n
theorem tendsto_nhds_of_cauchy_seq_of_subseq {α : Type u} {β : Type v} {u : β → α} (hu : cauchy_seq u) {ι : Type u_1} {f : ι → β} {p : filter ι} [p.ne_bot] (hf : filter.at_top) {a : α} (ha : filter.tendsto (u f) p (𝓝 a)) :
(𝓝 a)

If a Cauchy sequence has a convergent subsequence, then it converges.

@[nolint]
theorem filter.has_basis.cauchy_seq_iff {α : Type u} {β : Type v} {γ : Sort u_1} [nonempty β] {u : β → α} {p : γ → Prop} {s : γ → set × α)} (h : (𝓤 α).has_basis p s) :
∀ (i : γ), p i(∃ (N : β), ∀ (m n : β), m Nn N(u m, u n) s i)
theorem filter.has_basis.cauchy_seq_iff' {α : Type u} {β : Type v} {γ : Sort u_1} [nonempty β] {u : β → α} {p : γ → Prop} {s : γ → set × α)} (H : (𝓤 α).has_basis p s) :
∀ (i : γ), p i(∃ (N : β), ∀ (n : β), n N(u n, u N) s i)
theorem cauchy_seq_of_controlled {α : Type u} {β : Type v} [nonempty β] (U : β → set × α)) (hU : ∀ (s : set × α)), s 𝓤 α(∃ (n : β), U n s)) {f : β → α} (hf : ∀ {N m n : β}, N mN n(f m, f n) U N) :
@[class]
structure complete_space (α : Type u)  :
Prop
• complete : ∀ {f : filter α}, (∃ (x : α), f 𝓝 x)

A complete space is defined here using uniformities. A uniform space is complete if every Cauchy filter converges.

Instances
theorem complete_univ {α : Type u}  :
theorem cauchy_prod {α : Type u} {β : Type v} {f : filter α} {g : filter β} :
cauchy (f ×ᶠ g)
@[instance]
def complete_space.prod {α : Type u} {β : Type v}  :

If univ is complete, the space is a complete space

theorem complete_space_iff_is_complete_univ {α : Type u}  :
theorem cauchy_iff_exists_le_nhds {α : Type u} {l : filter α} [l.ne_bot] :
∃ (x : α), l 𝓝 x
theorem cauchy_map_iff_exists_tendsto {α : Type u} {β : Type v} {l : filter β} {f : β → α} [l.ne_bot] :
cauchy l) ∃ (x : α), (𝓝 x)
theorem cauchy_seq_tendsto_of_complete {α : Type u} {β : Type v} {u : β → α} (H : cauchy_seq u) :
∃ (x : α), (𝓝 x)

A Cauchy sequence in a complete space converges

theorem cauchy_seq_tendsto_of_is_complete {α : Type u} {β : Type v} {K : set α} (h₁ : is_complete K) {u : β → α} (h₂ : ∀ (n : β), u n K) (h₃ : cauchy_seq u) :
∃ (v : α) (H : v K), (𝓝 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} [nonempty α] {f : filter α} (hf : cauchy f) :
f 𝓝 (Lim f)
theorem cauchy_seq.tendsto_lim {α : Type u} {β : Type v} [nonempty α] {u : β → α} (h : cauchy_seq u) :
(𝓝 u))
theorem is_closed.is_complete {α : Type u} {s : set α} (h : is_closed s) :
def totally_bounded {α : Type u} (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_iff_subset {α : Type u} {s : set α} :
∀ (d : set × α)), d 𝓤 α(∃ (t : set α) (H : t s), t.finite s ⋃ (y : α) (H : y t), {x : α | (x, y) d})
theorem totally_bounded_of_forall_symm {α : Type u} {s : set α} (h : ∀ (V : set × α)), V 𝓤 α(∃ (t : set α), t.finite s ⋃ (y : α) (H : y t), ) :
theorem totally_bounded_subset {α : Type u} {s₁ s₂ : set α} (hs : s₁ s₂) (h : totally_bounded s₂) :
theorem totally_bounded_empty {α : Type u}  :
theorem totally_bounded.closure {α : Type u} {s : set α} (h : totally_bounded s) :

The closure of a totally bounded set is totally bounded.

theorem totally_bounded.image {α : Type u} {β : Type v} {f : α → β} {s : set α} (hs : totally_bounded s) (hf : uniform_continuous f) :

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

theorem ultrafilter.cauchy_of_totally_bounded {α : Type u} {s : set α} (f : ultrafilter α) (hs : totally_bounded s) (h : f 𝓟 s) :
theorem totally_bounded_iff_filter {α : Type u} {s : set α} :
∀ (f : filter α), f.ne_botf 𝓟 s(∃ (c : filter α) (H : c f), cauchy c)
theorem totally_bounded_iff_ultrafilter {α : Type u} {s : set α} :
∀ (f : , f 𝓟 s
theorem compact_iff_totally_bounded_complete {α : Type u} {s : set α} :
theorem is_compact.totally_bounded {α : Type u} {s : set α} (h : is_compact s) :
theorem is_compact.is_complete {α : Type u} {s : set α} (h : is_compact s) :
@[instance]
def complete_of_compact {α : Type u}  :
theorem compact_of_totally_bounded_is_closed {α : Type u} {s : set α} (ht : totally_bounded s) (hc : is_closed s) :

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

def sequentially_complete.set_seq_aux {α : Type u} {f : filter α} (hf : cauchy f) {U : set × α)} (U_mem : ∀ (n : ), U n 𝓤 α) (n : ) :
{s // ∃ (_x : s f), s.prod s U n}

An auxiliary sequence of sets approximating a Cauchy filter.

Equations
def sequentially_complete.set_seq {α : Type u} {f : filter α} (hf : cauchy f) {U : set × α)} (U_mem : ∀ (n : ), U n 𝓤 α) (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).prod (s n) ⊆ U.

Equations
theorem sequentially_complete.set_seq_mem {α : Type u} {f : filter α} (hf : cauchy f) {U : set × α)} (U_mem : ∀ (n : ), U n 𝓤 α) (n : ) :
U_mem n f
theorem sequentially_complete.set_seq_mono {α : Type u} {f : filter α} (hf : cauchy f) {U : set × α)} (U_mem : ∀ (n : ), U n 𝓤 α) ⦃m n : (h : m n) :
U_mem n U_mem m
theorem sequentially_complete.set_seq_sub_aux {α : Type u} {f : filter α} (hf : cauchy f) {U : set × α)} (U_mem : ∀ (n : ), U n 𝓤 α) (n : ) :
U_mem n U_mem n)
theorem sequentially_complete.set_seq_prod_subset {α : Type u} {f : filter α} (hf : cauchy f) {U : set × α)} (U_mem : ∀ (n : ), U n 𝓤 α) {N m n : } (hm : N m) (hn : N n) :
U_mem m).prod U_mem n) U N
def sequentially_complete.seq {α : Type u} {f : filter α} (hf : cauchy f) {U : set × α)} (U_mem : ∀ (n : ), U n 𝓤 α) (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
• U_mem n =
theorem sequentially_complete.seq_mem {α : Type u} {f : filter α} (hf : cauchy f) {U : set × α)} (U_mem : ∀ (n : ), U n 𝓤 α) (n : ) :
U_mem n U_mem n
theorem sequentially_complete.seq_pair_mem {α : Type u} {f : filter α} (hf : cauchy f) {U : set × α)} (U_mem : ∀ (n : ), U n 𝓤 α) ⦃N m n : (hm : N m) (hn : N n) :
U_mem m, U_mem n) U N
theorem sequentially_complete.seq_is_cauchy_seq {α : Type u} {f : filter α} (hf : cauchy f) {U : set × α)} (U_mem : ∀ (n : ), U n 𝓤 α) (U_le : ∀ (s : set × α)), s 𝓤 α(∃ (n : ), U n s)) :
cauchy_seq U_mem)
theorem sequentially_complete.le_nhds_of_seq_tendsto_nhds {α : Type u} {f : filter α} (hf : cauchy f) {U : set × α)} (U_mem : ∀ (n : ), U n 𝓤 α) (U_le : ∀ (s : set × α)), s 𝓤 α(∃ (n : ), U n s)) ⦃a : α⦄ (ha : (𝓝 a)) :
f 𝓝 a

If the sequence sequentially_complete.seq converges to a, then f ≤ 𝓝 a.

theorem uniform_space.complete_of_convergent_controlled_sequences {α : Type u} (H : (𝓤 α).is_countably_generated) (U : set × α)) (U_mem : ∀ (n : ), U n 𝓤 α) (HU : ∀ (u : → α), (∀ (N m n : ), N mN n(u m, u n) U N)(∃ (a : α), (𝓝 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} (H : (𝓤 α).is_countably_generated) (H' : ∀ (u : → α), (∃ (a : α), (𝓝 a))) :

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.