Theorems · Theorem · general topology

UniformSpace.complete_of_convergent_controlled_sequences

∀ {α : Type u} [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated] (U : ℕ → SetRel α α),
  (∀ (n : ℕ), U n ∈ uniformity α) →
    (∀ (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.

Defined in

Mathlib.Topology.UniformSpace.Cauchy

Cited by

3 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

UniformSpaceFilter.IsCountablyGenerated