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} {ι : Sort u_1} {p : ι → Prop} {s : ι → set × α)} (h : (uniformity α).has_basis p s) {f : filter α} :
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} {f : filter α} :
f.ne_bot ∀ (s : set × α)), s (∃ (t : set α) (H : t f), ∀ (x : α), x t∀ (y : α), y t(x, y) s)
theorem cauchy_iff {α : Type u} {f : filter α} :
f.ne_bot ∀ (s : set × α)), s (∃ (t : set α) (H : t f), t ×ˢ t s)
theorem cauchy.ultrafilter_of {α : Type u} {l : filter α} (h : cauchy l) :
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.prod l) (uniformity α)
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.prod l) (uniformity α)
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 : (nhds a)) :
theorem cauchy.prod {α : Type u} {β : Type v} {f : filter α} {g : filter β} (hf : cauchy f) (hg : cauchy g) :
cauchy (f.prod g)
theorem le_nhds_of_cauchy_adhp_aux {α : Type u} {f : filter α} {x : α} (adhs : ∀ (s : set × α)), s (∃ (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} {f : filter α} {x : α} (hf : cauchy f) (adhs : 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} {f : filter α} {x : α} (hf : cauchy f) :
f nhds 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)) (uniformity β) ) [ 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)) (uniformity β) ) (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.tendsto_uniformity {α : Type u} {β : Type v} {u : β → α} (h : cauchy_seq u) :
theorem cauchy_seq.nonempty {α : Type u} {β : Type v} {u : β → α} (hu : cauchy_seq u) :
theorem cauchy_seq.mem_entourage {α : Type u} {β : Type u_1} {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 : (nhds x)) :
theorem cauchy_seq_const {α : Type u} {β : Type v} [nonempty β] (x : α) :
cauchy_seq (λ (n : β), x)
theorem cauchy_seq_iff_tendsto {α : Type u} {β : Type v} [nonempty β] {u : β → α} :
theorem cauchy_seq.comp_tendsto {α : Type u} {β : Type v} {γ : Type u_1} [nonempty γ] {f : β → α} (hf : cauchy_seq f) {g : γ → β}  :
theorem cauchy_seq.comp_injective {α : Type u} {β : Type v} [no_max_order β] [nonempty β] {u : → α} (hu : cauchy_seq u) {f : β → } (hf : function.injective f) :
theorem function.bijective.cauchy_seq_comp_iff {α : Type u} {f : } (hf : function.bijective f) (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.prod_map {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {u : γ → α} {v : δ → β} (hu : cauchy_seq u) (hv : cauchy_seq v) :
theorem cauchy_seq.prod {α : Type u} {β : Type v} {γ : Type u_1} {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} {u : β → α} (hu : cauchy_seq u) {V : set × α)} (hV : V ) :
∀ᶠ (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} {γ : Type u_1} {f : α → β} (hf : uniform_continuous f) {u : γ → α} (hu : cauchy_seq u) :
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 filter.tendsto.subseq_mem_entourage {α : Type u} {V : set × α)} (hV : ∀ (n : ), V n ) {u : → α} {a : α} (hu : (nhds a)) :
∃ (φ : ), (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} {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 (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} {γ : Sort u_1} [nonempty β] {u : β → α} {p : γ → Prop} {s : γ → set × α)} (h : (uniformity α).has_basis p s) :
∀ (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} {γ : Sort u_1} [nonempty β] {u : β → α} {p : γ → Prop} {s : γ → set × α)} (H : (uniformity α).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) :
theorem is_complete_iff_cluster_pt {α : Type u} {s : set α} :
∀ (l : filter α), (∃ (x : α) (H : x s), l)
theorem is_complete_iff_ultrafilter {α : Type u} {s : set α} :
∀ (l : , (∃ (x : α) (H : x s), l nhds x)
theorem is_complete_iff_ultrafilter' {α : Type u} {s : set α} :
∀ (l : , s l(∃ (x : α) (H : x s), l nhds x)
@[protected]
theorem is_complete.union {α : Type u} {s t : set α} (hs : is_complete s) (ht : is_complete t) :
theorem is_complete_Union_separated {α : Type u} {ι : Sort u_1} {s : ι → set α} (hs : ∀ (i : ι), is_complete (s i)) {U : set × α)} (hU : U ) (hd : ∀ (i j : ι) (x : α), x s i∀ (y : α), y s j(x, y) Ui = j) :
is_complete (⋃ (i : ι), s i)
@[class]
structure complete_space (α : Type u)  :
Prop
• complete : ∀ {f : filter α}, (∃ (x : α), f nhds x)

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

Instances of this typeclass
theorem complete_univ {α : Type u}  :
@[protected, 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 complete_space_iff_ultrafilter {α : Type u}  :
∀ (l : , (∃ (x : α), l nhds x)
theorem cauchy_iff_exists_le_nhds {α : Type u} {l : filter α} [l.ne_bot] :
∃ (x : α), l nhds x
theorem cauchy_map_iff_exists_tendsto {α : Type u} {β : Type v} {l : filter β} {f : β → α} [l.ne_bot] :
cauchy l) ∃ (x : α), (nhds x)
theorem cauchy_seq_tendsto_of_complete {α : Type u} {β : Type v} {u : β → α} (H : cauchy_seq u) :
∃ (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),

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 nhds (Lim f)
theorem cauchy_seq.tendsto_lim {α : Type u} {β : Type v} [nonempty α] {u : β → α} (h : cauchy_seq 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.exists_subset {α : Type u} {s : set α} (hs : totally_bounded s) {U : set × α)} (hU : U ) :
∃ (t : set α) (H : t s), t.finite s ⋃ (y : α) (H : y t), {x : α | (x, y) U}
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 filter.has_basis.totally_bounded_iff {α : Type u} {ι : Sort u_1} {p : ι → Prop} {U : ι → set × α)} (H : (uniformity α).has_basis p U) {s : set α} :
∀ (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} {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 uniformly continuous map is totally bounded.

theorem ultrafilter.cauchy_of_totally_bounded {α : Type u} {s : set α} (f : ultrafilter α) (hs : totally_bounded s) (h : f ) :
theorem totally_bounded_iff_filter {α : Type u} {s : set α} :
∀ (f : filter α), f.ne_bot(∃ (c : filter α) (H : c f), cauchy c)
theorem totally_bounded_iff_ultrafilter {α : Type u} {s : set α} :
∀ (f : ,
theorem compact_iff_totally_bounded_complete {α : Type u} {s : set α} :
@[protected]
theorem is_compact.totally_bounded {α : Type u} {s : set α} (h : is_compact s) :
@[protected]
theorem is_compact.is_complete {α : Type u} {s : set α} (h : is_compact s) :
@[protected, 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.

noncomputable 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 ×ˢ 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 ×ˢ 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 ×ˢ U_mem n U N
noncomputable 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 : (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} (U : set × α)) (U_mem : ∀ (n : ), U n ) (HU : ∀ (u : → α), (∀ (N m n : ), N mN n(u m, u n) U N)(∃ (a : α), (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} (H' : ∀ (u : → α), (∃ (a : α), (nhds a))) :

A sequentially complete uniform space with a countable basis of the uniformity filter is complete.

@[protected, instance]

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.