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

def Cauchy {α : Type u} [uniformSpace : UniformSpace α] (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.NeBot ∧ f ×ˢ f ≤ uniformity α)

def IsComplete {α : Type u} [uniformSpace : UniformSpace α] (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

• IsComplete s = ∀ (f : Filter α), Cauchy f → f ≤ Filter.principal s → ∃ x ∈ s, f ≤ nhds x

theorem Filter.HasBasis.cauchy_iff {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} {p : ι → Prop} {s : ι → Set (α × α)} (h : (uniformity α).HasBasis p s) {f : Filter α} : Cauchy f ↔ f.NeBot ∧ ∀ (i : ι), p i → ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s i

theorem cauchy_iff' {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} : Cauchy f ↔ f.NeBot ∧ ∀ s ∈ uniformity α, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s

theorem cauchy_iff {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} : Cauchy f ↔ f.NeBot ∧ ∀ s ∈ uniformity α, ∃ t ∈ f, t ×ˢ t ⊆ s

theorem cauchy_iff_le {α : Type u} [uniformSpace : UniformSpace α] {l : Filter α} [hl : l.NeBot] : Cauchy l ↔ l ×ˢ l ≤ uniformity α

theorem Cauchy.ultrafilter_of {α : Type u} [uniformSpace : UniformSpace α] {l : Filter α} (h : Cauchy l) : Cauchy ↑(Ultrafilter.of l)

theorem cauchy_map_iff {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {l : Filter β} {f : β → α} : Cauchy (Filter.map f l) ↔ l.NeBot ∧ Filter.Tendsto (fun (p : β × β) => (f p.1, f p.2)) (l ×ˢ l) (uniformity α)

theorem cauchy_map_iff' {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {l : Filter β} [hl : l.NeBot] {f : β → α} : Cauchy (Filter.map f l) ↔ Filter.Tendsto (fun (p : β × β) => (f p.1, f p.2)) (l ×ˢ l) (uniformity α)

theorem Cauchy.mono {α : Type u} [uniformSpace : UniformSpace α] {f g : Filter α} [hg : g.NeBot] (h_c : Cauchy f) (h_le : g ≤ f) : Cauchy g

theorem Cauchy.mono' {α : Type u} [uniformSpace : UniformSpace α] {f g : Filter α} (h_c : Cauchy f) : g.NeBot → ∀ (h_le : g ≤ f), Cauchy g

theorem cauchy_nhds {α : Type u} [uniformSpace : UniformSpace α] {a : α} : Cauchy (nhds a)

theorem cauchy_pure {α : Type u} [uniformSpace : UniformSpace α] {a : α} : Cauchy (pure a)

theorem Filter.Tendsto.cauchy_map {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {l : Filter β} [l.NeBot] {f : β → α} {a : α} (h : Filter.Tendsto f l (nhds a)) : Cauchy (Filter.map f l)

theorem Cauchy.mono_uniformSpace {β : Type v} {u v : UniformSpace β} {F : Filter β} (huv : u ≤ v) (hF : Cauchy F) : Cauchy F

theorem cauchy_inf_uniformSpace {β : Type v} {u v : UniformSpace β} {F : Filter β} : Cauchy F ↔ Cauchy F ∧ Cauchy F

theorem cauchy_iInf_uniformSpace {β : Type v} {ι : Sort u_1} [Nonempty ι] {u : ι → UniformSpace β} {l : Filter β} : Cauchy l ↔ ∀ (i : ι), Cauchy l

theorem cauchy_iInf_uniformSpace' {β : Type v} {ι : Sort u_1} {u : ι → UniformSpace β} {l : Filter β} [l.NeBot] : Cauchy l ↔ ∀ (i : ι), Cauchy l

theorem cauchy_comap_uniformSpace {β : Type v} {u : UniformSpace β} {α : Type u_1} {f : α → β} {l : Filter α} : Cauchy l ↔ Cauchy (Filter.map f l)

theorem cauchy_prod_iff {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] {F : Filter (α × β)} : Cauchy F ↔ Cauchy (Filter.map Prod.fst F) ∧ Cauchy (Filter.map Prod.snd F)

theorem Cauchy.prod {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] {f : Filter α} {g : Filter β} (hf : Cauchy f) (hg : Cauchy g) : Cauchy (f ×ˢ g)

theorem le_nhds_of_cauchy_adhp_aux {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} {x : α} (adhs : ∀ s ∈ uniformity α, ∃ 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 SequentiallyComplete.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} [uniformSpace : UniformSpace α] {f : Filter α} {x : α} (hf : Cauchy f) (adhs : ClusterPt 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} [uniformSpace : UniformSpace α] {f : Filter α} {x : α} (hf : Cauchy f) : f ≤ nhds x ↔ ClusterPt x f

theorem Cauchy.map {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] {f : Filter α} {m : α → β} (hf : Cauchy f) (hm : UniformContinuous m) : Cauchy (Filter.map m f)

theorem Cauchy.comap {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] {f : Filter β} {m : α → β} (hf : Cauchy f) (hm : Filter.comap (fun (p : α × α) => (m p.1, m p.2)) (uniformity β) ≤ uniformity α) [(Filter.comap m f).NeBot] : Cauchy (Filter.comap m f)

theorem Cauchy.comap' {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] {f : Filter β} {m : α → β} (hf : Cauchy f) (hm : Filter.comap (fun (p : α × α) => (m p.1, m p.2)) (uniformity β) ≤ uniformity α) : (Filter.comap m f).NeBot → Cauchy (Filter.comap m f)

def CauchySeq {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Preorder β] (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

• CauchySeq u = Cauchy (Filter.map u Filter.atTop)

theorem CauchySeq.tendsto_uniformity {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Preorder β] {u : β → α} (h : CauchySeq u) : Filter.Tendsto (Prod.map u u) Filter.atTop (uniformity α)

theorem CauchySeq.nonempty {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Preorder β] {u : β → α} (hu : CauchySeq u) : Nonempty β

theorem CauchySeq.mem_entourage {α : Type u} [uniformSpace : UniformSpace α] {β : Type u_1} [SemilatticeSup β] {u : β → α} (h : CauchySeq u) {V : Set (α × α)} (hV : V ∈ uniformity α) : ∃ (k₀ : β), ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V

theorem Filter.Tendsto.cauchySeq {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [SemilatticeSup β] [Nonempty β] {f : β → α} {x : α} (hx : Filter.Tendsto f Filter.atTop (nhds x)) : CauchySeq f

theorem cauchySeq_const {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [SemilatticeSup β] [Nonempty β] (x : α) : CauchySeq fun (x_1 : β) => x

theorem cauchySeq_iff_tendsto {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Nonempty β] [SemilatticeSup β] {u : β → α} : CauchySeq u ↔ Filter.Tendsto (Prod.map u u) Filter.atTop (uniformity α)

theorem CauchySeq.comp_tendsto {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Type u_1} [Preorder β] [SemilatticeSup γ] [Nonempty γ] {f : β → α} (hf : CauchySeq f) {g : γ → β} (hg : Filter.Tendsto g Filter.atTop Filter.atTop) : CauchySeq (f ∘ g)

theorem CauchySeq.comp_injective {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [SemilatticeSup β] [NoMaxOrder β] [Nonempty β] {u : ℕ → α} (hu : CauchySeq u) {f : β → ℕ} (hf : Function.Injective f) : CauchySeq (u ∘ f)

theorem Function.Bijective.cauchySeq_comp_iff {α : Type u} [uniformSpace : UniformSpace α] {f : ℕ → ℕ} (hf : Function.Bijective f) (u : ℕ → α) : CauchySeq (u ∘ f) ↔ CauchySeq u

theorem CauchySeq.subseq_subseq_mem {α : Type u} [uniformSpace : UniformSpace α] {V : ℕ → Set (α × α)} (hV : ∀ (n : ℕ), V n ∈ uniformity α) {u : ℕ → α} (hu : CauchySeq u) {f g : ℕ → ℕ} (hf : Filter.Tendsto f Filter.atTop Filter.atTop) (hg : Filter.Tendsto g Filter.atTop Filter.atTop) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n

theorem cauchySeq_iff' {α : Type u} [uniformSpace : UniformSpace α] {u : ℕ → α} : CauchySeq u ↔ ∀ V ∈ uniformity α, ∀ᶠ (k : ℕ × ℕ) in Filter.atTop, k ∈ Prod.map u u ⁻¹' V

theorem cauchySeq_iff {α : Type u} [uniformSpace : UniformSpace α] {u : ℕ → α} : CauchySeq u ↔ ∀ V ∈ uniformity α, ∃ (N : ℕ), ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V

theorem CauchySeq.prod_map {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Type u_1} {δ : Type u_2} [UniformSpace β] [Preorder γ] [Preorder δ] {u : γ → α} {v : δ → β} (hu : CauchySeq u) (hv : CauchySeq v) : CauchySeq (Prod.map u v)

theorem CauchySeq.prod {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Type u_1} [UniformSpace β] [Preorder γ] {u : γ → α} {v : γ → β} (hu : CauchySeq u) (hv : CauchySeq v) : CauchySeq fun (x : γ) => (u x, v x)

theorem CauchySeq.eventually_eventually {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [SemilatticeSup β] {u : β → α} (hu : CauchySeq u) {V : Set (α × α)} (hV : V ∈ uniformity α) : ∀ᶠ (k : β) (l : β) in Filter.atTop, (u k, u l) ∈ V

theorem UniformContinuous.comp_cauchySeq {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Type u_1} [UniformSpace β] [Preorder γ] {f : α → β} (hf : UniformContinuous f) {u : γ → α} (hu : CauchySeq u) : CauchySeq (f ∘ u)

theorem CauchySeq.subseq_mem {α : Type u} [uniformSpace : UniformSpace α] {V : ℕ → Set (α × α)} (hV : ∀ (n : ℕ), V n ∈ uniformity α) {u : ℕ → α} (hu : CauchySeq u) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V n

theorem Filter.Tendsto.subseq_mem_entourage {α : Type u} [uniformSpace : UniformSpace α] {V : ℕ → Set (α × α)} (hV : ∀ (n : ℕ), V n ∈ uniformity α) {u : ℕ → α} {a : α} (hu : Filter.Tendsto u Filter.atTop (nhds a)) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1)

theorem tendsto_nhds_of_cauchySeq_of_subseq {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Preorder β] {u : β → α} (hu : CauchySeq u) {ι : Type u_1} {f : ι → β} {p : Filter ι} [p.NeBot] (hf : Filter.Tendsto f p Filter.atTop) {a : α} (ha : Filter.Tendsto (u ∘ f) p (nhds a)) : Filter.Tendsto u Filter.atTop (nhds a)

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

theorem cauchySeq_shift {α : Type u} [uniformSpace : UniformSpace α] {u : ℕ → α} (k : ℕ) : (CauchySeq fun (n : ℕ) => u (n + k)) ↔ CauchySeq u

Any shift of a Cauchy sequence is also a Cauchy sequence.

theorem Filter.HasBasis.cauchySeq_iff {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Sort u_1} [Nonempty β] [SemilatticeSup β] {u : β → α} {p : γ → Prop} {s : γ → Set (α × α)} (h : (uniformity α).HasBasis p s) : CauchySeq u ↔ ∀ (i : γ), p i → ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i

theorem Filter.HasBasis.cauchySeq_iff' {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Sort u_1} [Nonempty β] [SemilatticeSup β] {u : β → α} {p : γ → Prop} {s : γ → Set (α × α)} (H : (uniformity α).HasBasis p s) : CauchySeq u ↔ ∀ (i : γ), p i → ∃ (N : β), ∀ n ≥ N, (u n, u N) ∈ s i

theorem cauchySeq_of_controlled {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [SemilatticeSup β] [Nonempty β] (U : β → Set (α × α)) (hU : ∀ s ∈ uniformity α, ∃ (n : β), U n ⊆ s) {f : β → α} (hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N) : CauchySeq f

theorem isComplete_iff_clusterPt {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} : IsComplete s ↔ ∀ (l : Filter α), Cauchy l → l ≤ Filter.principal s → ∃ x ∈ s, ClusterPt x l

theorem isComplete_iff_ultrafilter {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} : IsComplete s ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ Filter.principal s → ∃ x ∈ s, ↑l ≤ nhds x

theorem isComplete_iff_ultrafilter' {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} : IsComplete s ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → s ∈ l → ∃ x ∈ s, ↑l ≤ nhds x

theorem IsComplete.union {α : Type u} [uniformSpace : UniformSpace α] {s t : Set α} (hs : IsComplete s) (ht : IsComplete t) : IsComplete (s ∪ t)

theorem isComplete_iUnion_separated {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} {s : ι → Set α} (hs : ∀ (i : ι), IsComplete (s i)) {U : Set (α × α)} (hU : U ∈ uniformity α) (hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j) : IsComplete (⋃ (i : ι), s i)

class CompleteSpace (α : Type u) [UniformSpace α] : Prop

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

• complete {f : Filter α} : Cauchy f → ∃ (x : α), f ≤ nhds x

  In a complete uniform space, every Cauchy filter converges.

theorem complete_univ {α : Type u} [UniformSpace α] [CompleteSpace α] : IsComplete Set.univ

instance CompleteSpace.prod {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] [CompleteSpace α] [CompleteSpace β] : CompleteSpace (α × β)

theorem CompleteSpace.fst_of_prod {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] [CompleteSpace (α × β)] [h : Nonempty β] : CompleteSpace α

theorem CompleteSpace.snd_of_prod {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] [CompleteSpace (α × β)] [h : Nonempty α] : CompleteSpace β

theorem completeSpace_prod_of_nonempty {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] [Nonempty α] [Nonempty β] : CompleteSpace (α × β) ↔ CompleteSpace α ∧ CompleteSpace β

instance CompleteSpace.mulOpposite {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] : CompleteSpace αᵐᵒᵖ

instance CompleteSpace.addOpposite {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] : CompleteSpace αᵃᵒᵖ

theorem completeSpace_of_isComplete_univ {α : Type u} [uniformSpace : UniformSpace α] (h : IsComplete Set.univ) : CompleteSpace α

If univ is complete, the space is a complete space

theorem completeSpace_iff_isComplete_univ {α : Type u} [uniformSpace : UniformSpace α] : CompleteSpace α ↔ IsComplete Set.univ

theorem completeSpace_iff_ultrafilter {α : Type u} [uniformSpace : UniformSpace α] : CompleteSpace α ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → ∃ (x : α), ↑l ≤ nhds x

theorem cauchy_iff_exists_le_nhds {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] {l : Filter α} [l.NeBot] : Cauchy l ↔ ∃ (x : α), l ≤ nhds x

theorem cauchy_map_iff_exists_tendsto {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [CompleteSpace α] {l : Filter β} {f : β → α} [l.NeBot] : Cauchy (Filter.map f l) ↔ ∃ (x : α), Filter.Tendsto f l (nhds x)

theorem cauchySeq_tendsto_of_complete {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Preorder β] [CompleteSpace α] {u : β → α} (H : CauchySeq u) : ∃ (x : α), Filter.Tendsto u Filter.atTop (nhds x)

A Cauchy sequence in a complete space converges

theorem cauchySeq_tendsto_of_isComplete {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Preorder β] {K : Set α} (h₁ : IsComplete K) {u : β → α} (h₂ : ∀ (n : β), u n ∈ K) (h₃ : CauchySeq u) : ∃ v ∈ K, Filter.Tendsto u Filter.atTop (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} [uniformSpace : UniformSpace α] [CompleteSpace α] {f : Filter α} (hf : Cauchy f) : f ≤ nhds (lim f)

theorem CauchySeq.tendsto_limUnder {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Preorder β] [CompleteSpace α] {u : β → α} (h : CauchySeq u) : Filter.Tendsto u Filter.atTop (nhds (limUnder Filter.atTop u))

theorem IsClosed.isComplete {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] {s : Set α} (h : IsClosed s) : IsComplete s

def TotallyBounded {α : Type u} [uniformSpace : UniformSpace α] (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

• TotallyBounded s = ∀ d ∈ uniformity α, ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ d}

theorem TotallyBounded.exists_subset {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (hs : TotallyBounded s) {U : Set (α × α)} (hU : U ∈ uniformity α) : ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U}

theorem totallyBounded_iff_subset {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} : TotallyBounded s ↔ ∀ d ∈ uniformity α, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ d}

theorem Filter.HasBasis.totallyBounded_iff {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} {p : ι → Prop} {U : ι → Set (α × α)} (H : (uniformity α).HasBasis p U) {s : Set α} : TotallyBounded s ↔ ∀ (i : ι), p i → ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U i}

theorem totallyBounded_of_forall_symm {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (h : ∀ V ∈ uniformity α, SymmetricRel V → ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, UniformSpace.ball y V) : TotallyBounded s

theorem TotallyBounded.subset {α : Type u} [uniformSpace : UniformSpace α] {s₁ s₂ : Set α} (hs : s₁ ⊆ s₂) (h : TotallyBounded s₂) : TotallyBounded s₁

@[deprecated TotallyBounded.subset]

theorem totallyBounded_subset {α : Type u} [uniformSpace : UniformSpace α] {s₁ s₂ : Set α} (hs : s₁ ⊆ s₂) (h : TotallyBounded s₂) : TotallyBounded s₁

Alias of TotallyBounded.subset.

theorem TotallyBounded.closure {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (h : TotallyBounded s) : TotallyBounded (closure s)

The closure of a totally bounded set is totally bounded.

@[simp]

theorem totallyBounded_closure {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} : TotallyBounded (closure s) ↔ TotallyBounded s

@[simp]

theorem totallyBounded_iUnion {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} [Finite ι] {s : ι → Set α} : TotallyBounded (⋃ (i : ι), s i) ↔ ∀ (i : ι), TotallyBounded (s i)

A finite indexed union is totally bounded if and only if each set of the family is totally bounded.

theorem totallyBounded_biUnion {α : Type u} [uniformSpace : UniformSpace α] {ι : Type u_1} {I : Set ι} (hI : I.Finite) {s : ι → Set α} : TotallyBounded (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, TotallyBounded (s i)

A union indexed by a finite set is totally bounded if and only if each set of the family is totally bounded.

theorem totallyBounded_sUnion {α : Type u} [uniformSpace : UniformSpace α] {S : Set (Set α)} (hS : S.Finite) : TotallyBounded (⋃₀ S) ↔ ∀ s ∈ S, TotallyBounded s

A union of a finite family of sets is totally bounded if and only if each set of the family is totally bounded.

theorem Set.Finite.totallyBounded {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (hs : s.Finite) : TotallyBounded s

A finite set is totally bounded.

theorem Set.Subsingleton.totallyBounded {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (hs : s.Subsingleton) : TotallyBounded s

A subsingleton is totally bounded.

@[simp]

theorem totallyBounded_singleton {α : Type u} [uniformSpace : UniformSpace α] (a : α) : TotallyBounded {a}

@[simp]

theorem totallyBounded_empty {α : Type u} [uniformSpace : UniformSpace α] : TotallyBounded ∅

@[simp]

theorem totallyBounded_union {α : Type u} [uniformSpace : UniformSpace α] {s t : Set α} : TotallyBounded (s ∪ t) ↔ TotallyBounded s ∧ TotallyBounded t

The union of two sets is totally bounded if and only if each of the two sets is totally bounded.

theorem TotallyBounded.union {α : Type u} [uniformSpace : UniformSpace α] {s t : Set α} (hs : TotallyBounded s) (ht : TotallyBounded t) : TotallyBounded (s ∪ t)

The union of two totally bounded sets is totally bounded.

@[simp]

theorem totallyBounded_insert {α : Type u} [uniformSpace : UniformSpace α] (a : α) {s : Set α} : TotallyBounded (insert a s) ↔ TotallyBounded s

theorem TotallyBounded.insert {α : Type u} [uniformSpace : UniformSpace α] (a : α) {s : Set α} : TotallyBounded s → TotallyBounded (insert a s)

Alias of the reverse direction of totallyBounded_insert.

theorem TotallyBounded.image {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] {f : α → β} {s : Set α} (hs : TotallyBounded s) (hf : UniformContinuous f) : TotallyBounded (f '' s)

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

theorem Ultrafilter.cauchy_of_totallyBounded {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (f : Ultrafilter α) (hs : TotallyBounded s) (h : ↑f ≤ Filter.principal s) : Cauchy ↑f

theorem totallyBounded_iff_filter {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} : TotallyBounded s ↔ ∀ (f : Filter α), f.NeBot → f ≤ Filter.principal s → ∃ c ≤ f, Cauchy c

theorem totallyBounded_iff_ultrafilter {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} : TotallyBounded s ↔ ∀ (f : Ultrafilter α), ↑f ≤ Filter.principal s → Cauchy ↑f

theorem isCompact_iff_totallyBounded_isComplete {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} : IsCompact s ↔ TotallyBounded s ∧ IsComplete s

theorem IsCompact.totallyBounded {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (h : IsCompact s) : TotallyBounded s

theorem IsCompact.isComplete {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (h : IsCompact s) : IsComplete s

@[instance 100]

instance complete_of_compact {α : Type u} [UniformSpace α] [CompactSpace α] : CompleteSpace α

theorem isCompact_of_totallyBounded_isClosed {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] {s : Set α} (ht : TotallyBounded s) (hc : IsClosed s) : IsCompact s

theorem CauchySeq.totallyBounded_range {α : Type u} [uniformSpace : UniformSpace α] {s : ℕ → α} (hs : CauchySeq s) : TotallyBounded (Set.range 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/MetricSpace/EmetricSpace and Topology/MetricSpace/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 SequentiallyComplete.setSeqAux {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → Set (α × α)} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (n : ℕ) : { s : Set α // s ∈ f ∧ s ×ˢ s ⊆ U n }

An auxiliary sequence of sets approximating a Cauchy filter.

Equations

• SequentiallyComplete.setSeqAux hf U_mem n = Classical.indefiniteDescription (fun (s : Set α) => s ∈ f ∧ s ×ˢ s ⊆ U n) ⋯

def SequentiallyComplete.setSeq {α : Type u} [uniformSpace : UniformSpace α] {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

• SequentiallyComplete.setSeq hf U_mem n = ⋂ m ∈ Set.Iic n, ↑(SequentiallyComplete.setSeqAux hf U_mem m)

theorem SequentiallyComplete.setSeq_mem {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → Set (α × α)} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (n : ℕ) : SequentiallyComplete.setSeq hf U_mem n ∈ f

theorem SequentiallyComplete.setSeq_mono {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → Set (α × α)} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) ⦃m n : ℕ⦄ (h : m ≤ n) : SequentiallyComplete.setSeq hf U_mem n ⊆ SequentiallyComplete.setSeq hf U_mem m

theorem SequentiallyComplete.setSeq_sub_aux {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → Set (α × α)} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (n : ℕ) : SequentiallyComplete.setSeq hf U_mem n ⊆ ↑(SequentiallyComplete.setSeqAux hf U_mem n)

theorem SequentiallyComplete.setSeq_prod_subset {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → Set (α × α)} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) {N m n : ℕ} (hm : N ≤ m) (hn : N ≤ n) : SequentiallyComplete.setSeq hf U_mem m ×ˢ SequentiallyComplete.setSeq hf U_mem n ⊆ U N

def SequentiallyComplete.seq {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → Set (α × α)} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (n : ℕ) : α

A sequence of points such that seq n ∈ setSeq n. Here setSeq is an antitone sequence of sets setSeq n ∈ f with diameters controlled by a given sequence of entourages.

Equations

• SequentiallyComplete.seq hf U_mem n = Exists.choose ⋯

theorem SequentiallyComplete.seq_mem {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → Set (α × α)} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (n : ℕ) : SequentiallyComplete.seq hf U_mem n ∈ SequentiallyComplete.setSeq hf U_mem n

theorem SequentiallyComplete.seq_pair_mem {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → Set (α × α)} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) ⦃N m n : ℕ⦄ (hm : N ≤ m) (hn : N ≤ n) : (SequentiallyComplete.seq hf U_mem m, SequentiallyComplete.seq hf U_mem n) ∈ U N

theorem SequentiallyComplete.seq_is_cauchySeq {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → Set (α × α)} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (U_le : ∀ s ∈ uniformity α, ∃ (n : ℕ), U n ⊆ s) : CauchySeq (SequentiallyComplete.seq hf U_mem)

theorem SequentiallyComplete.le_nhds_of_seq_tendsto_nhds {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → Set (α × α)} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (U_le : ∀ s ∈ uniformity α, ∃ (n : ℕ), U n ⊆ s) ⦃a : α⦄ (ha : Filter.Tendsto (SequentiallyComplete.seq hf U_mem) Filter.atTop (nhds a)) : f ≤ nhds a

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

theorem UniformSpace.complete_of_convergent_controlled_sequences {α : Type u} [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated] (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.atTop (nhds a)) : CompleteSpace α

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 UniformSpace.complete_of_cauchySeq_tendsto {α : Type u} [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated] (H' : ∀ (u : ℕ → α), CauchySeq u → ∃ (a : α), Filter.Tendsto u Filter.atTop (nhds a)) : CompleteSpace α

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

@[instance 100]

instance UniformSpace.firstCountableTopology (α : Type u) [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated] : FirstCountableTopology α

theorem UniformSpace.secondCountable_of_separable (α : Type u) [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated] [TopologicalSpace.SeparableSpace α] : SecondCountableTopology α

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.

theorem UniformSpace.DiscreteUnif.cauchy_le_pure {X : Type u_1} {uX : UniformSpace X} (hX : uX = ⊥) {α : Filter X} (hα : Cauchy α) : ∃ (x : X), α = pure x

A Cauchy filter in a discrete uniform space is contained in a principal filter

noncomputable def UniformSpace.DiscreteUnif.cauchyConst {X : Type u_1} {uX : UniformSpace X} (hX : uX = ⊥) {α : Filter X} (hα : Cauchy α) : X

A constant to which a Cauchy filter in a discrete uniform space converges.

Equations

• UniformSpace.DiscreteUnif.cauchyConst hX hα = ⋯.choose

theorem UniformSpace.DiscreteUnif.eq_const_of_cauchy {X : Type u_1} {uX : UniformSpace X} (hX : uX = ⊥) {α : Filter X} (hα : Cauchy α) : α = pure (UniformSpace.DiscreteUnif.cauchyConst hX hα)