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.

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

theorem Filter.HasBasis.cauchy_iff {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} {p : ι → Prop} {s : ι → SetRel α α} (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 : Tendsto f l (nhds a)) : Cauchy (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.

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 : SetRel α α} (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 : Tendsto f 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 : Bijective f) (u : ℕ → α) : CauchySeq (u ∘ f) ↔ CauchySeq u

theorem CauchySeq.subseq_subseq_mem {α : Type u} [uniformSpace : UniformSpace α] {V : ℕ → SetRel α α} (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.prodMap {α : 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.prodMk {α : 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 α] [Preorder β] {u : β → α} (hu : CauchySeq u) {V : SetRel α α} (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 : ℕ → SetRel α α} (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 : ℕ → SetRel α α} (hV : ∀ (n : ℕ), V n ∈ uniformity α) {u : ℕ → α} {a : α} (hu : Tendsto u 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 : γ → SetRel α α} (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 : γ → SetRel α α} (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 : β → SetRel α α) (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 : SetRel α α} (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

theorem DiscreteUniformity.eq_pure_of_cauchy {α : Type u} [uniformSpace : UniformSpace α] [DiscreteUniformity α] {f : Filter α} (hf : Cauchy f) : ∃ (x : α), f = pure x

A Cauchy filter in a discrete uniform space is contained in the principal filter of a point.

instance DiscreteUniformity.instCompleteSpace {α : Type u} [uniformSpace : UniformSpace α] [DiscreteUniformity α] : CompleteSpace α

The discrete uniformity makes a space complete.

noncomputable def DiscreteUniformity.cauchyConst {α : Type u} [uniformSpace : UniformSpace α] [DiscreteUniformity α] {f : Filter α} (hf : Cauchy f) : α

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

theorem DiscreteUniformity.eq_pure_cauchyConst {α : Type u} [uniformSpace : UniformSpace α] [DiscreteUniformity α] {f : Filter α} (hf : Cauchy f) : f = pure (cauchyConst hf)

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.

def Filter.TotallyBounded {α : Type u} [uniformSpace : UniformSpace α] (f : Filter α) : Prop

A filter f is totally bounded if for every entourage d, the d-neighborhood of some finite set is in f.

theorem Filter.totallyBounded_principal_iff {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} : (principal s).TotallyBounded ↔ TotallyBounded s

theorem Filter.TotallyBounded.exists_subset_of_mem {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : f.TotallyBounded) {s : Set α} (hs : s ∈ f) {U : SetRel α α} (hU : U ∈ uniformity α) : ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f

theorem TotallyBounded.exists_subset {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (hs : TotallyBounded s) {U : SetRel α α} (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 : ι → SetRel α α} (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 Filter.HasBasis.filter_totallyBounded_iff {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} {p : ι → Prop} {U : ι → SetRel α α} (H : (uniformity α).HasBasis p U) {f : Filter α} : f.TotallyBounded ↔ ∀ (i : ι), p i → ∃ (t : Set α), t.Finite ∧ (U i).preimage t ∈ f

theorem totallyBounded_of_forall_isSymm {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (h : ∀ V ∈ uniformity α, SetRel.IsSymm 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₁

theorem Filter.TotallyBounded.mono {α : Type u} [uniformSpace : UniformSpace α] {f g : Filter α} (h : f ≤ g) (hg : g.TotallyBounded) : f.TotallyBounded

theorem Filter.TotallyBounded.totallyBounded_setOf_clusterPt {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (h : f.TotallyBounded) : TotallyBounded {x : α | ClusterPt x f}

theorem TotallyBounded.closure {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (h : TotallyBounded s) : TotallyBounded (_root_.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 Filter.totallyBounded_iSup {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} [Finite ι] {f : ι → Filter α} : (⨆ (i : ι), f i).TotallyBounded ↔ ∀ (i : ι), (f i).TotallyBounded

theorem Filter.totallyBounded_biSup {α : Type u} [uniformSpace : UniformSpace α] {ι : Type u_1} {I : Set ι} (hI : I.Finite) {f : ι → Filter α} : (⨆ i ∈ I, f i).TotallyBounded ↔ ∀ i ∈ I, (f i).TotallyBounded

theorem totallyBounded_sSup {α : Type u} [uniformSpace : UniformSpace α] {S : Set (Filter α)} (hS : S.Finite) : (sSup S).TotallyBounded ↔ ∀ f ∈ S, f.TotallyBounded

@[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 Filter.totallyBounded_bot {α : 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.

@[simp]

theorem Filter.totallyBounded_sup {α : Type u} [uniformSpace : UniformSpace α] {f g : Filter α} : (f ⊔ g).TotallyBounded ↔ f.TotallyBounded ∧ g.TotallyBounded

theorem Filter.TotallyBounded.sup {α : Type u} [uniformSpace : UniformSpace α] {f g : Filter α} (hf : f.TotallyBounded) (hg : g.TotallyBounded) : (f ⊔ g).TotallyBounded

theorem Filter.TotallyBounded.map {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] {f : α → β} {g : Filter α} (hg : g.TotallyBounded) (hf : UniformContinuous f) : (Filter.map f g).TotallyBounded

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 α] (f : Ultrafilter α) (hf : (↑f).TotallyBounded) : Cauchy ↑f

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

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

theorem Filter.totallyBounded_iff_ultrafilter {α : Type u} [uniformSpace : UniformSpace α] {g : Filter α} : g.TotallyBounded ↔ ∀ (f : Ultrafilter α), ↑f ≤ g → 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 TotallyBounded.isCompact_of_isComplete {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (ht : TotallyBounded s) (hc : IsComplete s) : IsCompact s

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

@[deprecated TotallyBounded.isCompact_of_isClosed (since := "2025-08-30")]

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

Alias of TotallyBounded.isCompact_of_isClosed.

theorem Filter.TotallyBounded.isCompact_setOf_clusterPt {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] {f : Filter α} (hf : f.TotallyBounded) : IsCompact {x : α | ClusterPt x f}

theorem Filter.TotallyBounded.exists_clusterPt {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] {f : Filter α} [f.NeBot] (hf : f.TotallyBounded) : ∃ (x : α), ClusterPt x f

theorem CauchySeq.totallyBounded_range {α : Type u} [uniformSpace : UniformSpace α] {s : ℕ → α} (hs : CauchySeq s) : TotallyBounded (Set.range s)

Every Cauchy sequence over ℕ is totally bounded.

def interUnionBalls {α : Type u} (xs : ℕ → α) (u : ℕ → ℕ) (V : ℕ → SetRel α α) : Set α

Given a family of points xs n, a family of entourages V n of the diagonal and a family of natural numbers u n, the intersection over n of the V n-neighborhood of xs 1, ..., xs (u n). Designed to be relatively compact when V n tends to the diagonal.

theorem totallyBounded_interUnionBalls {α : Type u} [uniformSpace : UniformSpace α] {p : ℕ → Prop} {U : ℕ → SetRel α α} (H : (uniformity α).HasBasis p U) (xs : ℕ → α) (u : ℕ → ℕ) : TotallyBounded (interUnionBalls xs u U)

theorem isCompact_closure_interUnionBalls {α : Type u} [uniformSpace : UniformSpace α] {p : ℕ → Prop} {U : ℕ → SetRel α α} (H : (uniformity α).HasBasis p U) [CompleteSpace α] (xs : ℕ → α) (u : ℕ → ℕ) : IsCompact (closure (interUnionBalls xs u U))

The construction interUnionBalls is used to have a relatively compact set.

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 Mathlib/Topology/EMetricSpace/Basic.lean and Mathlib/Topology/MetricSpace/Basic.lean.

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 : ℕ → SetRel α α} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (n : ℕ) : { s : Set α // s ∈ f ∧ s ×ˢ s ⊆ U n }

An auxiliary sequence of sets approximating a Cauchy filter.

def SequentiallyComplete.setSeq {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α} (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.

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

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

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

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

def SequentiallyComplete.seq {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α} (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.

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

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

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

theorem SequentiallyComplete.le_nhds_of_seq_tendsto_nhds {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (U_le : ∀ s ∈ uniformity α, ∃ (n : ℕ), U n ⊆ s) ⦃a : α⦄ (ha : Filter.Tendsto (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 : ℕ → SetRel α α) (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 α

instance 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 𝓤 α.

theorem UniformSpace.subset_countable_closure_of_almost_dense_set {α : Type u} [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated] (s : Set α) (hs : ∀ U ∈ uniformity α, ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x U) : ∃ t ⊆ s, t.Countable ∧ s ⊆ closure t

theorem UniformSpace.secondCountable_of_almost_dense_set {α : Type u} [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated] (hs : ∀ U ∈ uniformity α, ∃ (t : Set α), t.Countable ∧ ⋃ x ∈ t, ball x U = Set.univ) : SecondCountableTopology α

theorem TotallyBounded.isSeparable {α : Type u} [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated] {s : Set α} (h : TotallyBounded s) : TopologicalSpace.IsSeparable s

A totally bounded set is separable in countably generated uniform spaces. This can be obtained from the more general UniformSpace.subset_countable_closure_of_almost_dense_set.