Documentation

Mathlib.Topology.UniformSpace.Cauchy

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

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

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 : 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
    Instances For
      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 itf, xt, yt, (x, y) s i
      theorem cauchy_iff' {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} :
      Cauchy f f.NeBot suniformity α, tf, xt, yt, (x, y) s
      theorem cauchy_iff {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} :
      Cauchy f f.NeBot suniformity α, tf, t ×ˢ t s
      theorem cauchy_iff_le {α : Type u} [uniformSpace : UniformSpace α] {l : Filter α} [hl : l.NeBot] :
      theorem Cauchy.ultrafilter_of {α : Type u} [uniformSpace : UniformSpace α] {l : Filter α} (h : Cauchy 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 : Filter α} {g : Filter α} [hg : g.NeBot] (h_c : Cauchy f) (h_le : g f) :
      theorem Cauchy.mono' {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} {g : Filter α} (h_c : Cauchy f) :
      g.NeBotg fCauchy g
      theorem cauchy_nhds {α : Type u} [uniformSpace : UniformSpace α] {a : α} :
      theorem cauchy_pure {α : Type u} [uniformSpace : UniformSpace α] {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)) :
      theorem Cauchy.mono_uniformSpace {β : Type v} {u : UniformSpace β} {v : UniformSpace β} {F : Filter β} (huv : u v) (hF : Cauchy F) :
      theorem cauchy_inf_uniformSpace {β : Type v} {u : UniformSpace β} {v : UniformSpace β} {F : Filter β} :
      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 α} :
      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 : suniformity α, 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 : 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) :
      theorem Cauchy.map {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] {f : Filter α} {m : αβ} (hf : Cauchy f) (hm : UniformContinuous m) :
      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] :
      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).NeBotCauchy (Filter.comap m f)
      def CauchySeq {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Preorder β] (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 : 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) :
        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₀ ik₀ 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)) :
        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) :
        theorem CauchySeq.comp_injective {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [SemilatticeSup β] [NoMaxOrder β] [Nonempty β] {u : α} (hu : CauchySeq u) {f : β} (hf : Function.Injective f) :
        theorem Function.Bijective.cauchySeq_comp_iff {α : Type u} [uniformSpace : UniformSpace α] {f : } (hf : Function.Bijective f) (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 Vuniformity α, ∀ᶠ (k : × ) in Filter.atTop, k Prod.map u u ⁻¹' V
        theorem cauchySeq_iff {α : Type u} [uniformSpace : UniformSpace α] {u : α} :
        CauchySeq u Vuniformity α, ∃ (N : ), kN, lN, (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) :
        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) :
        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 : β), nN, (u n, u N) s i
        theorem cauchySeq_of_controlled {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [SemilatticeSup β] [Nonempty β] (U : βSet (α × α)) (hU : suniformity α, ∃ (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 : UniformSpace α] {s : Set α} :
        IsComplete s ∀ (l : Filter α), Cauchy ll Filter.principal sxs, ClusterPt x l
        theorem isComplete_iff_ultrafilter {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} :
        IsComplete s ∀ (l : Ultrafilter α), Cauchy ll Filter.principal sxs, l nhds x
        theorem isComplete_iff_ultrafilter' {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} :
        IsComplete s ∀ (l : Ultrafilter α), Cauchy ls lxs, l nhds x
        theorem IsComplete.union {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} {t : Set α} (hs : IsComplete s) (ht : IsComplete 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 : ι), xs i, ys j, (x, y) Ui = j) :
        IsComplete (⋃ (i : ι), s i)
        class CompleteSpace (α : Type u) [UniformSpace α] :

        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.

        Instances
          theorem CompleteSpace.complete {α : Type u} [UniformSpace α] [self : CompleteSpace α] {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 β] :
          Equations
          • =
          theorem CompleteSpace.fst_of_prod {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] [CompleteSpace (α × β)] [h : Nonempty β] :
          theorem CompleteSpace.snd_of_prod {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] [CompleteSpace (α × β)] [h : Nonempty α] :
          theorem completeSpace_prod_of_nonempty {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] [Nonempty α] [Nonempty β] :
          instance CompleteSpace.addOpposite {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] :
          Equations
          • =
          instance CompleteSpace.mulOpposite {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] :
          Equations
          • =
          theorem completeSpace_of_isComplete_univ {α : Type u} [uniformSpace : UniformSpace α] (h : IsComplete Set.univ) :

          If univ is complete, the space is a complete space

          theorem completeSpace_iff_isComplete_univ {α : Type u} [uniformSpace : UniformSpace α] :
          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) :
          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 : 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) :
          def TotallyBounded {α : Type u} [uniformSpace : 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
          Instances For
            theorem TotallyBounded.exists_subset {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (hs : TotallyBounded s) {U : Set (α × α)} (hU : U uniformity α) :
            ts, t.Finite s yt, {x : α | (x, y) U}
            theorem totallyBounded_iff_subset {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} :
            TotallyBounded s duniformity α, ts, t.Finite s yt, {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 yt, {x : α | (x, y) U i}
            theorem totallyBounded_of_forall_symm {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (h : Vuniformity α, SymmetricRel V∃ (t : Set α), t.Finite s yt, UniformSpace.ball y V) :
            theorem TotallyBounded.subset {α : Type u} [uniformSpace : UniformSpace α] {s₁ : Set α} {s₂ : Set α} (hs : s₁ s₂) (h : TotallyBounded s₂) :
            @[deprecated TotallyBounded.subset]
            theorem totallyBounded_subset {α : Type u} [uniformSpace : UniformSpace α] {s₁ : Set α} {s₂ : Set α} (hs : s₁ s₂) (h : TotallyBounded s₂) :

            Alias of TotallyBounded.subset.

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

            The closure of a totally bounded set is totally bounded.

            @[simp]
            theorem totallyBounded_closure {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} :
            @[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 (⋃ 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 : UniformSpace α] {S : Set (Set α)} (hS : S.Finite) :

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

            A finite set is totally bounded.

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

            A subsingleton is totally bounded.

            @[simp]
            theorem totallyBounded_singleton {α : Type u} [uniformSpace : UniformSpace α] (a : α) :
            @[simp]
            theorem totallyBounded_empty {α : Type u} [uniformSpace : UniformSpace α] :
            @[simp]
            theorem totallyBounded_union {α : Type u} [uniformSpace : 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 : UniformSpace α] {s : Set α} {t : Set α} (hs : TotallyBounded s) (ht : TotallyBounded t) :

            The union of two totally bounded sets is totally bounded.

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

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

            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.NeBotf Filter.principal scf, Cauchy c
            theorem totallyBounded_iff_ultrafilter {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} :
            TotallyBounded s ∀ (f : Ultrafilter α), f Filter.principal sCauchy f
            theorem IsCompact.totallyBounded {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (h : IsCompact s) :
            theorem IsCompact.isComplete {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (h : IsCompact s) :
            @[instance 100]
            Equations
            • =
            theorem isCompact_of_totallyBounded_isClosed {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] {s : Set α} (ht : TotallyBounded s) (hc : IsClosed s) :
            theorem CauchySeq.totallyBounded_range {α : Type u} [uniformSpace : UniformSpace α] {s : α} (hs : CauchySeq 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
            Instances For
              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
              Instances For
                theorem SequentiallyComplete.setSeq_mem {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : Set (α × α)} (U_mem : ∀ (n : ), U n uniformity α) (n : ) :
                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) :
                theorem SequentiallyComplete.setSeq_sub_aux {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : Set (α × α)} (U_mem : ∀ (n : ), U n uniformity α) (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) :
                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
                Instances For
                  theorem SequentiallyComplete.seq_mem {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : Set (α × α)} (U_mem : ∀ (n : ), U n uniformity α) (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) :
                  theorem SequentiallyComplete.seq_is_cauchySeq {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : Set (α × α)} (U_mem : ∀ (n : ), U n uniformity α) (U_le : suniformity α, ∃ (n : ), U n s) :
                  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 : suniformity α, ∃ (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 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 : UniformSpace α] [(uniformity α).IsCountablyGenerated] (H' : ∀ (u : α), CauchySeq 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 : UniformSpace α] [(uniformity α).IsCountablyGenerated] :
                  Equations
                  • =

                  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.