mathlib documentation

topology.uniform_space.cauchy

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

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

cauchy f = (f.ne_bot ∧ f ×ᶠ f ≤ 𝓤 α)

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

is_complete s = ∀ (f : filter α), cauchy f → f ≤ 𝓟 s → (∃ (x : α) (H : x ∈ s), f ≤ 𝓝 x)

theorem filter.has_basis.cauchy_iff {α : Type u} {β : Type v} [uniform_space α] {p : β → Prop} {s : β → set (α × α)} (h : (𝓤 α).has_basis p s) {f : filter α} :

cauchy f ↔ f.ne_bot ∧ ∀ (i : β), p i → (∃ (t : set α) (H : t ∈ f), ∀ (x y : α), x ∈ t → y ∈ t → (x, y) ∈ s i)

theorem cauchy_iff' {α : Type u} [uniform_space α] {f : filter α} :

cauchy f ↔ f.ne_bot ∧ ∀ (s : set (α × α)), s ∈ 𝓤 α → (∃ (t : set α) (H : t ∈ f), ∀ (x y : α), x ∈ t → y ∈ t → (x, y) ∈ s)

theorem cauchy_iff {α : Type u} [uniform_space α] {f : filter α} :

cauchy f ↔ f.ne_bot ∧ ∀ (s : set (α × α)), s ∈ 𝓤 α → (∃ (t : set α) (H : t ∈ f), t.prod t ⊆ 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 ×ᶠ l) (𝓤 α)

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 ×ᶠ l) (𝓤 α)

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 : α} :

cauchy (𝓝 a)

theorem cauchy_pure {α : Type u} [uniform_space α] {a : α} :

cauchy (pure a)

theorem le_nhds_of_cauchy_adhp_aux {α : Type u} [uniform_space α] {f : filter α} {x : α} (adhs : ∀ (s : set (α × α)), s ∈ 𝓤 α → (∃ (t : set α) (H : t ∈ f), t.prod 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 ≤ 𝓝 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)) (𝓤 β) ≤ 𝓤 α) [(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)) (𝓤 β) ≤ 𝓤 α) (hb : (filter.comap m f).ne_bot) :

cauchy (filter.comap m f)

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

cauchy_seq u = cauchy (filter.map u filter.at_top)

theorem cauchy_seq.mem_entourage {α : Type u} [uniform_space α] {ι : Type u_1} [nonempty ι] [decidable_linear_order ι] {u : ι → α} (h : cauchy_seq u) {V : set (α × α)} (hV : V ∈ 𝓤 α) :

∃ (k₀ : ι), ∀ (i j : ι), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V

theorem cauchy_seq_of_tendsto_nhds {α : Type u} {β : Type v} [uniform_space α] [semilattice_sup β] [nonempty β] (f : β → α) {x : α} (hx : filter.tendsto f filter.at_top (𝓝 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 (𝓤 α)

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 (𝓝 a)) :

filter.tendsto u filter.at_top (𝓝 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 α] {γ : Type u_1} [nonempty β] [semilattice_sup β] {u : β → α} {p : γ → Prop} {s : γ → set (α × α)} (h : (𝓤 α).has_basis p s) :

cauchy_seq u ↔ ∀ (i : γ), p i → (∃ (N : β), ∀ (m n : β), m ≥ N → n ≥ N → (u m, u n) ∈ s i)

theorem filter.has_basis.cauchy_seq_iff' {α : Type u} {β : Type v} [uniform_space α] {γ : Type u_1} [nonempty β] [semilattice_sup β] {u : β → α} {p : γ → Prop} {s : γ → set (α × α)} (H : (𝓤 α).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 ∈ 𝓤 α → (∃ (n : β), U n ⊆ s)) {f : β → α} (hf : ∀ {N m n : β}, N ≤ m → N ≤ n → (f m, f n) ∈ U N) :

@[class]

structure complete_space (α : Type u) [uniform_space α] :

Prop

complete : ∀ {f : filter α}, cauchy f → (∃ (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} [uniform_space α] [complete_space α] :

is_complete set.univ

theorem cauchy_prod {α : Type u} {β : Type v} [uniform_space α] [uniform_space β] {f : filter α} {g : filter β} (a : cauchy f) (a_1 : cauchy g) :

cauchy (f ×ᶠ g)

@[instance]

def complete_space.prod {α : Type u} {β : Type v} [uniform_space α] [uniform_space β] [complete_space α] [complete_space β] :

complete_space (α × β)

theorem complete_space_of_is_complete_univ {α : Type u} [uniform_space α] (h : is_complete set.univ) :

complete_space α

If univ is complete, the space is a complete space

theorem complete_space_iff_is_complete_univ {α : Type u} [uniform_space α] :

complete_space α ↔ is_complete set.univ

theorem cauchy_iff_exists_le_nhds {α : Type u} [uniform_space α] [complete_space α] {l : filter α} [l.ne_bot] :

cauchy l ↔ ∃ (x : α), l ≤ 𝓝 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 (𝓝 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 (𝓝 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 (𝓝 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 ≤ 𝓝 (Lim 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 (𝓝 (lim filter.at_top u))

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

totally_bounded s = ∀ (d : set (α × α)), d ∈ 𝓤 α → (∃ (t : set α), t.finite ∧ s ⊆ ⋃ (y : α) (H : y ∈ t), {x : α | (x, y) ∈ d})

theorem totally_bounded_iff_subset {α : Type u} [uniform_space α] {s : set α} :

totally_bounded s ↔ ∀ (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} [uniform_space α] {s : set α} (h : ∀ (V : set (α × α)), V ∈ 𝓤 α → symmetric_rel V → (∃ (t : set α), t.finite ∧ s ⊆ ⋃ (y : α) (H : y ∈ t), uniform_space.ball y V)) :

totally_bounded s

theorem totally_bounded_subset {α : Type u} [uniform_space α] {s₁ s₂ : set α} (hs : s₁ ⊆ s₂) (h : totally_bounded s₂) :

totally_bounded s₁

theorem totally_bounded_empty {α : Type u} [uniform_space α] :

totally_bounded ∅

theorem totally_bounded.closure {α : Type u} [uniform_space α] {s : set α} (h : totally_bounded s) :

totally_bounded (closure 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 unifromly continuous map is totally bounded.

theorem cauchy_of_totally_bounded_of_ultrafilter {α : Type u} [uniform_space α] {s : set α} {f : filter α} (hs : totally_bounded s) (hf : f.is_ultrafilter) (h : f ≤ 𝓟 s) :

theorem totally_bounded_iff_filter {α : Type u} [uniform_space α] {s : set α} :

totally_bounded s ↔ ∀ (f : filter α), f.ne_bot → f ≤ 𝓟 s → (∃ (c : filter α) (H : c ≤ f), cauchy c)

theorem totally_bounded_iff_ultrafilter {α : Type u} [uniform_space α] {s : set α} :

totally_bounded s ↔ ∀ (f : filter α), f.is_ultrafilter → f ≤ 𝓟 s → cauchy f

theorem compact_iff_totally_bounded_complete {α : Type u} [uniform_space α] {s : set α} :

is_compact s ↔ totally_bounded s ∧ is_complete s

@[instance]

def complete_of_compact {α : Type u} [uniform_space α] [compact_space α] :

complete_space α

theorem compact_of_totally_bounded_is_closed {α : Type u} [uniform_space α] [complete_space α] {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} [uniform_space α] {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

sequentially_complete.set_seq_aux hf U_mem n = classical.indefinite_description (λ (s : set α), ∃ (_x : s ∈ f), s.prod s ⊆ U n) _

def sequentially_complete.set_seq {α : Type u} [uniform_space α] {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 a sequence of monotonically decreasing sets s n ∈ f such that (s n).prod (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 ∈ 𝓤 α) (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 ∈ 𝓤 α) ⦃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 ∈ 𝓤 α) (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 ∈ 𝓤 α) {N m n : ℕ} (hm : N ≤ m) (hn : N ≤ n) :

(sequentially_complete.set_seq hf U_mem m).prod (sequentially_complete.set_seq hf U_mem n) ⊆ U N

def sequentially_complete.seq {α : Type u} [uniform_space α] {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 a monotonically decreasing 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 ∈ 𝓤 α) (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 ∈ 𝓤 α) ⦃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 ∈ 𝓤 α) (U_le : ∀ (s : set (α × α)), s ∈ 𝓤 α → (∃ (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 ∈ 𝓤 α) (U_le : ∀ (s : set (α × α)), s ∈ 𝓤 α → (∃ (n : ℕ), U n ⊆ s)) ⦃a : α⦄ (ha : filter.tendsto (sequentially_complete.seq hf U_mem) filter.at_top (𝓝 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 α] (H : (𝓤 α).is_countably_generated) (U : ℕ → set (α × α)) (U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α) (HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → (∃ (a : α), filter.tendsto u filter.at_top (𝓝 a))) :

complete_space α

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 α] (H : (𝓤 α).is_countably_generated) (H' : ∀ (u : ℕ → α), cauchy_seq u → (∃ (a : α), filter.tendsto u filter.at_top (𝓝 a))) :

complete_space α

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

theorem uniform_space.first_countable_topology {α : Type u} [uniform_space α] (H : (𝓤 α).is_countably_generated) :

topological_space.first_countable_topology α