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

def Cauchy {α : Type u} [uniformSpace : ] (f : ) :

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
Instances For
def IsComplete {α : Type u} [uniformSpace : ] (s : Set α) :

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
• = ∀ (f : ), xs, f nhds x
Instances For
theorem Filter.HasBasis.cauchy_iff {α : Type u} [uniformSpace : ] {ι : Sort u_1} {p : ιProp} {s : ιSet (α × α)} (h : ().HasBasis p s) {f : } :
f.NeBot ∀ (i : ι), p itf, xt, yt, (x, y) s i
theorem cauchy_iff' {α : Type u} [uniformSpace : ] {f : } :
f.NeBot s, tf, xt, yt, (x, y) s
theorem cauchy_iff {α : Type u} [uniformSpace : ] {f : } :
f.NeBot s, tf, t ×ˢ t s
theorem cauchy_iff_le {α : Type u} [uniformSpace : ] {l : } [hl : l.NeBot] :
l ×ˢ l
theorem Cauchy.ultrafilter_of {α : Type u} [uniformSpace : ] {l : } (h : ) :
Cauchy ()
theorem cauchy_map_iff {α : Type u} {β : Type v} [uniformSpace : ] {l : } {f : βα} :
Cauchy () l.NeBot Filter.Tendsto (fun (p : β × β) => (f p.1, f p.2)) (l ×ˢ l) ()
theorem cauchy_map_iff' {α : Type u} {β : Type v} [uniformSpace : ] {l : } [hl : l.NeBot] {f : βα} :
Cauchy () Filter.Tendsto (fun (p : β × β) => (f p.1, f p.2)) (l ×ˢ l) ()
theorem Cauchy.mono {α : Type u} [uniformSpace : ] {f : } {g : } [hg : g.NeBot] (h_c : ) (h_le : g f) :
theorem Cauchy.mono' {α : Type u} [uniformSpace : ] {f : } {g : } (h_c : ) :
g.NeBotg f
theorem cauchy_nhds {α : Type u} [uniformSpace : ] {a : α} :
theorem cauchy_pure {α : Type u} [uniformSpace : ] {a : α} :
theorem Filter.Tendsto.cauchy_map {α : Type u} {β : Type v} [uniformSpace : ] {l : } [l.NeBot] {f : βα} {a : α} (h : Filter.Tendsto f l (nhds a)) :
theorem Cauchy.mono_uniformSpace {β : Type v} {u : } {v : } {F : } (huv : u v) (hF : ) :
theorem cauchy_inf_uniformSpace {β : Type v} {u : } {v : } {F : } :
theorem cauchy_iInf_uniformSpace {β : Type v} {ι : Sort u_1} [] {u : ι} {l : } :
∀ (i : ι),
theorem cauchy_iInf_uniformSpace' {β : Type v} {ι : Sort u_1} {u : ι} {l : } [l.NeBot] :
∀ (i : ι),
theorem cauchy_comap_uniformSpace {α : Type u} {β : Type v} {u : } {f : αβ} {l : } :
theorem cauchy_prod_iff {α : Type u} {β : Type v} [uniformSpace : ] [] {F : Filter (α × β)} :
Cauchy (Filter.map Prod.fst F) Cauchy (Filter.map Prod.snd F)
theorem Cauchy.prod {α : Type u} {β : Type v} [uniformSpace : ] [] {f : } {g : } (hf : ) (hg : ) :
Cauchy (f ×ˢ g)
theorem le_nhds_of_cauchy_adhp_aux {α : Type u} [uniformSpace : ] {f : } {x : α} (adhs : s, tf, 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 : ] {f : } {x : α} (hf : ) (adhs : ) :
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 : ] {f : } {x : α} (hf : ) :
f nhds x
theorem Cauchy.map {α : Type u} {β : Type v} [uniformSpace : ] [] {f : } {m : αβ} (hf : ) (hm : ) :
theorem Cauchy.comap {α : Type u} {β : Type v} [uniformSpace : ] [] {f : } {m : αβ} (hf : ) (hm : Filter.comap (fun (p : α × α) => (m p.1, m p.2)) () ) [().NeBot] :
theorem Cauchy.comap' {α : Type u} {β : Type v} [uniformSpace : ] [] {f : } {m : αβ} (hf : ) (hm : Filter.comap (fun (p : α × α) => (m p.1, m p.2)) () ) :
().NeBotCauchy ()
def CauchySeq {α : Type u} {β : Type v} [uniformSpace : ] [] (u : βα) :

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
Instances For
theorem CauchySeq.tendsto_uniformity {α : Type u} {β : Type v} [uniformSpace : ] [] {u : βα} (h : ) :
Filter.Tendsto (Prod.map u u) Filter.atTop ()
theorem CauchySeq.nonempty {α : Type u} {β : Type v} [uniformSpace : ] [] {u : βα} (hu : ) :
theorem CauchySeq.mem_entourage {α : Type u} [uniformSpace : ] {β : Type u_1} [] {u : βα} (h : ) {V : Set (α × α)} (hV : V ) :
∃ (k₀ : β), ∀ (i j : β), k₀ ik₀ j(u i, u j) V
theorem Filter.Tendsto.cauchySeq {α : Type u} {β : Type v} [uniformSpace : ] [] [] {f : βα} {x : α} (hx : Filter.Tendsto f Filter.atTop (nhds x)) :
theorem cauchySeq_const {α : Type u} {β : Type v} [uniformSpace : ] [] [] (x : α) :
CauchySeq fun (x_1 : β) => x
theorem cauchySeq_iff_tendsto {α : Type u} {β : Type v} [uniformSpace : ] [] [] {u : βα} :
Filter.Tendsto (Prod.map u u) Filter.atTop ()
theorem CauchySeq.comp_tendsto {α : Type u} {β : Type v} [uniformSpace : ] {γ : Type u_1} [] [] [] {f : βα} (hf : ) {g : γβ} (hg : Filter.Tendsto g Filter.atTop Filter.atTop) :
theorem CauchySeq.comp_injective {α : Type u} {β : Type v} [uniformSpace : ] [] [] [] {u : α} (hu : ) {f : β} (hf : ) :
theorem Function.Bijective.cauchySeq_comp_iff {α : Type u} [uniformSpace : ] {f : } (hf : ) (u : α) :
theorem CauchySeq.subseq_subseq_mem {α : Type u} [uniformSpace : ] {V : Set (α × α)} (hV : ∀ (n : ), V n ) {u : α} (hu : ) {f : } {g : } (hf : Filter.Tendsto f Filter.atTop Filter.atTop) (hg : Filter.Tendsto g Filter.atTop Filter.atTop) :
∃ (φ : ), ∀ (n : ), ((u f φ) n, (u g φ) n) V n
theorem cauchySeq_iff' {α : Type u} [uniformSpace : ] {u : α} :
V, ∀ᶠ (k : ) in Filter.atTop, k Prod.map u u ⁻¹' V
theorem cauchySeq_iff {α : Type u} [uniformSpace : ] {u : α} :
V, ∃ (N : ), kN, lN, (u k, u l) V
theorem CauchySeq.prod_map {α : Type u} {β : Type v} [uniformSpace : ] {γ : Type u_1} {δ : Type u_2} [] [] [] {u : γα} {v : δβ} (hu : ) (hv : ) :
theorem CauchySeq.prod {α : Type u} {β : Type v} [uniformSpace : ] {γ : Type u_1} [] [] {u : γα} {v : γβ} (hu : ) (hv : ) :
CauchySeq fun (x : γ) => (u x, v x)
theorem CauchySeq.eventually_eventually {α : Type u} {β : Type v} [uniformSpace : ] [] {u : βα} (hu : ) {V : Set (α × α)} (hV : V ) :
∀ᶠ (k : β) (l : β) in Filter.atTop, (u k, u l) V
theorem UniformContinuous.comp_cauchySeq {α : Type u} {β : Type v} [uniformSpace : ] {γ : Type u_1} [] [] {f : αβ} (hf : ) {u : γα} (hu : ) :
theorem CauchySeq.subseq_mem {α : Type u} [uniformSpace : ] {V : Set (α × α)} (hV : ∀ (n : ), V n ) {u : α} (hu : ) :
∃ (φ : ), ∀ (n : ), (u (φ (n + 1)), u (φ n)) V n
theorem Filter.Tendsto.subseq_mem_entourage {α : Type u} [uniformSpace : ] {V : Set (α × α)} (hV : ∀ (n : ), V n ) {u : α} {a : α} (hu : Filter.Tendsto u Filter.atTop (nhds a)) :
∃ (φ : ), (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 : ] [] {u : βα} (hu : ) {ι : Type u_1} {f : ιβ} {p : } [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 : ] {u : α} (k : ) :
(CauchySeq fun (n : ) => u (n + k))

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

theorem Filter.HasBasis.cauchySeq_iff {α : Type u} {β : Type v} [uniformSpace : ] {γ : Sort u_1} [] [] {u : βα} {p : γProp} {s : γSet (α × α)} (h : ().HasBasis p s) :
∀ (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 : ] {γ : Sort u_1} [] [] {u : βα} {p : γProp} {s : γSet (α × α)} (H : ().HasBasis p s) :
∀ (i : γ), p i∃ (N : β), nN, (u n, u N) s i
theorem cauchySeq_of_controlled {α : Type u} {β : Type v} [uniformSpace : ] [] [] (U : βSet (α × α)) (hU : s, ∃ (n : β), U n s) {f : βα} (hf : ∀ ⦃N m n : β⦄, N mN n(f m, f n) U N) :
theorem isComplete_iff_clusterPt {α : Type u} [uniformSpace : ] {s : Set α} :
∀ (l : ), xs,
theorem isComplete_iff_ultrafilter {α : Type u} [uniformSpace : ] {s : Set α} :
∀ (l : ), Cauchy lxs, l nhds x
theorem isComplete_iff_ultrafilter' {α : Type u} [uniformSpace : ] {s : Set α} :
∀ (l : ), Cauchy ls lxs, l nhds x
theorem IsComplete.union {α : Type u} [uniformSpace : ] {s : Set α} {t : Set α} (hs : ) (ht : ) :
theorem isComplete_iUnion_separated {α : Type u} [uniformSpace : ] {ι : Sort u_1} {s : ιSet α} (hs : ∀ (i : ι), IsComplete (s i)) {U : Set (α × α)} (hU : U ) (hd : ∀ (i j : ι), xs i, ys j, (x, y) Ui = j) :
IsComplete (⋃ (i : ι), s i)
class CompleteSpace (α : Type u) [] :

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

• complete : ∀ {f : }, ∃ (x : α), f nhds x

In a complete uniform space, every Cauchy filter converges.

Instances
theorem CompleteSpace.complete {α : Type u} [] [self : ] {f : } :
∃ (x : α), f nhds x

In a complete uniform space, every Cauchy filter converges.

theorem complete_univ {α : Type u} [] [] :
IsComplete Set.univ
instance CompleteSpace.prod {α : Type u} {β : Type v} [uniformSpace : ] [] [] [] :
Equations
• =
theorem CompleteSpace.fst_of_prod {α : Type u} {β : Type v} [uniformSpace : ] [] [CompleteSpace (α × β)] [h : ] :
theorem CompleteSpace.snd_of_prod {α : Type u} {β : Type v} [uniformSpace : ] [] [CompleteSpace (α × β)] [h : ] :
theorem completeSpace_prod_of_nonempty {α : Type u} {β : Type v} [uniformSpace : ] [] [] [] :
abbrev CompleteSpace.addOpposite.match_1 {α : Type u_1} [uniformSpace : ] :
∀ {f : } (motive : (∃ (x : α), Filter.map AddOpposite.unop f nhds x)Prop) (x : ∃ (x : α), Filter.map AddOpposite.unop f nhds x), (∀ (x : α) (hx : Filter.map AddOpposite.unop f nhds x), motive )motive x
Equations
• =
Instances For
instance CompleteSpace.addOpposite {α : Type u} [uniformSpace : ] [] :
Equations
• =
instance CompleteSpace.mulOpposite {α : Type u} [uniformSpace : ] [] :
Equations
• =
theorem completeSpace_of_isComplete_univ {α : Type u} [uniformSpace : ] (h : IsComplete Set.univ) :

If univ is complete, the space is a complete space

theorem completeSpace_iff_isComplete_univ {α : Type u} [uniformSpace : ] :
IsComplete Set.univ
theorem completeSpace_iff_ultrafilter {α : Type u} [uniformSpace : ] :
∀ (l : ), Cauchy l∃ (x : α), l nhds x
theorem cauchy_iff_exists_le_nhds {α : Type u} [uniformSpace : ] [] {l : } [l.NeBot] :
∃ (x : α), l nhds x
theorem cauchy_map_iff_exists_tendsto {α : Type u} {β : Type v} [uniformSpace : ] [] {l : } {f : βα} [l.NeBot] :
Cauchy () ∃ (x : α), Filter.Tendsto f l (nhds x)
theorem cauchySeq_tendsto_of_complete {α : Type u} {β : Type v} [uniformSpace : ] [] [] {u : βα} (H : ) :
∃ (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 : ] [] {K : Set α} (h₁ : ) {u : βα} (h₂ : ∀ (n : β), u n K) (h₃ : ) :
vK, 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 : ] [] {f : } (hf : ) :
f nhds (lim f)
theorem CauchySeq.tendsto_limUnder {α : Type u} {β : Type v} [uniformSpace : ] [] [] {u : βα} (h : ) :
Filter.Tendsto u Filter.atTop (nhds (limUnder Filter.atTop u))
theorem IsClosed.isComplete {α : Type u} [uniformSpace : ] [] {s : Set α} (h : ) :
def TotallyBounded {α : Type u} [uniformSpace : ] (s : Set α) :

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
• = d ∈ , ∃ (t : Set α), t.Finite s yt, {x : α | (x, y) d}
Instances For
theorem TotallyBounded.exists_subset {α : Type u} [uniformSpace : ] {s : Set α} (hs : ) {U : Set (α × α)} (hU : U ) :
ts, t.Finite s yt, {x : α | (x, y) U}
theorem totallyBounded_iff_subset {α : Type u} [uniformSpace : ] {s : Set α} :
d, ts, t.Finite s yt, {x : α | (x, y) d}
theorem Filter.HasBasis.totallyBounded_iff {α : Type u} [uniformSpace : ] {ι : Sort u_1} {p : ιProp} {U : ιSet (α × α)} (H : ().HasBasis p U) {s : Set α} :
∀ (i : ι), p i∃ (t : Set α), t.Finite s yt, {x : α | (x, y) U i}
theorem totallyBounded_of_forall_symm {α : Type u} [uniformSpace : ] {s : Set α} (h : V, ∃ (t : Set α), t.Finite s yt, ) :
theorem TotallyBounded.subset {α : Type u} [uniformSpace : ] {s₁ : Set α} {s₂ : Set α} (hs : s₁ s₂) (h : ) :
@[deprecated TotallyBounded.subset]
theorem totallyBounded_subset {α : Type u} [uniformSpace : ] {s₁ : Set α} {s₂ : Set α} (hs : s₁ s₂) (h : ) :

Alias of TotallyBounded.subset.

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

The closure of a totally bounded set is totally bounded.

@[simp]
theorem totallyBounded_closure {α : Type u} [uniformSpace : ] {s : Set α} :
@[simp]
theorem totallyBounded_iUnion {α : Type u} [uniformSpace : ] {ι : Sort u_1} [] {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 : ] {ι : Type u_1} {I : Set ι} (hI : I.Finite) {s : ιSet α} :
TotallyBounded (iI, s i) iI, 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 : ] {S : Set (Set α)} (hS : S.Finite) :
TotallyBounded (⋃₀ S) sS,

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 : ] {s : Set α} (hs : s.Finite) :

A finite set is totally bounded.

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

A subsingleton is totally bounded.

@[simp]
theorem totallyBounded_singleton {α : Type u} [uniformSpace : ] (a : α) :
@[simp]
theorem totallyBounded_empty {α : Type u} [uniformSpace : ] :
@[simp]
theorem totallyBounded_union {α : Type u} [uniformSpace : ] {s : Set α} {t : Set α} :

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 : ] {s : Set α} {t : Set α} (hs : ) (ht : ) :

The union of two totally bounded sets is totally bounded.

@[simp]
theorem totallyBounded_insert {α : Type u} [uniformSpace : ] (a : α) {s : Set α} :
theorem TotallyBounded.insert {α : Type u} [uniformSpace : ] (a : α) {s : Set α} :

Alias of the reverse direction of totallyBounded_insert.

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

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

theorem Ultrafilter.cauchy_of_totallyBounded {α : Type u} [uniformSpace : ] {s : Set α} (f : ) (hs : ) (h : ) :
Cauchy f
theorem totallyBounded_iff_filter {α : Type u} [uniformSpace : ] {s : Set α} :
∀ (f : ), f.NeBotcf,
theorem totallyBounded_iff_ultrafilter {α : Type u} [uniformSpace : ] {s : Set α} :
∀ (f : ), Cauchy f
theorem isCompact_iff_totallyBounded_isComplete {α : Type u} [uniformSpace : ] {s : Set α} :
theorem IsCompact.totallyBounded {α : Type u} [uniformSpace : ] {s : Set α} (h : ) :
theorem IsCompact.isComplete {α : Type u} [uniformSpace : ] {s : Set α} (h : ) :
@[instance 100]
instance complete_of_compact {α : Type u} [] [] :
Equations
• =
theorem isCompact_of_totallyBounded_isClosed {α : Type u} [uniformSpace : ] [] {s : Set α} (ht : ) (hc : ) :
theorem CauchySeq.totallyBounded_range {α : Type u} [uniformSpace : ] {s : α} (hs : ) :

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 : ] {f : } (hf : ) {U : Set (α × α)} (U_mem : ∀ (n : ), U n ) (n : ) :
{ s : Set α // s f s ×ˢ s U n }

An auxiliary sequence of sets approximating a Cauchy filter.

Equations
Instances For
def SequentiallyComplete.setSeq {α : Type u} [uniformSpace : ] {f : } (hf : ) {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
Instances For
theorem SequentiallyComplete.setSeq_mem {α : Type u} [uniformSpace : ] {f : } (hf : ) {U : Set (α × α)} (U_mem : ∀ (n : ), U n ) (n : ) :
theorem SequentiallyComplete.setSeq_mono {α : Type u} [uniformSpace : ] {f : } (hf : ) {U : Set (α × α)} (U_mem : ∀ (n : ), U n ) ⦃m : ⦃n : (h : m n) :
theorem SequentiallyComplete.setSeq_sub_aux {α : Type u} [uniformSpace : ] {f : } (hf : ) {U : Set (α × α)} (U_mem : ∀ (n : ), U n ) (n : ) :
theorem SequentiallyComplete.setSeq_prod_subset {α : Type u} [uniformSpace : ] {f : } (hf : ) {U : Set (α × α)} (U_mem : ∀ (n : ), U n ) {N : } {m : } {n : } (hm : N m) (hn : N n) :
def SequentiallyComplete.seq {α : Type u} [uniformSpace : ] {f : } (hf : ) {U : Set (α × α)} (U_mem : ∀ (n : ), U n ) (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
Instances For
theorem SequentiallyComplete.seq_mem {α : Type u} [uniformSpace : ] {f : } (hf : ) {U : Set (α × α)} (U_mem : ∀ (n : ), U n ) (n : ) :
theorem SequentiallyComplete.seq_pair_mem {α : Type u} [uniformSpace : ] {f : } (hf : ) {U : Set (α × α)} (U_mem : ∀ (n : ), U n ) ⦃N : ⦃m : ⦃n : (hm : N m) (hn : N n) :
theorem SequentiallyComplete.seq_is_cauchySeq {α : Type u} [uniformSpace : ] {f : } (hf : ) {U : Set (α × α)} (U_mem : ∀ (n : ), U n ) (U_le : s, ∃ (n : ), U n s) :
theorem SequentiallyComplete.le_nhds_of_seq_tendsto_nhds {α : Type u} [uniformSpace : ] {f : } (hf : ) {U : Set (α × α)} (U_mem : ∀ (n : ), U n ) (U_le : s, ∃ (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 : ] [().IsCountablyGenerated] (U : Set (α × α)) (U_mem : ∀ (n : ), U n ) (HU : ∀ (u : α), (∀ (N m n : ), N mN n(u m, u n) U N)∃ (a : α), Filter.Tendsto u Filter.atTop (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 UniformSpace.complete_of_cauchySeq_tendsto {α : Type u} [uniformSpace : ] [().IsCountablyGenerated] (H' : ∀ (u : α), ∃ (a : α), Filter.Tendsto u Filter.atTop (nhds a)) :

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

@[instance 100]
instance UniformSpace.firstCountableTopology (α : Type u) [uniformSpace : ] [().IsCountablyGenerated] :
Equations
• =
theorem UniformSpace.secondCountable_of_separable (α : Type u) [uniformSpace : ] [().IsCountablyGenerated] :

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.