Theorems · Theorem · general topology

Metric.complete_of_convergent_controlled_sequences

∀ {α : Type u} [inst : PseudoMetricSpace α] (B : ℕ → ℝ),
  (∀ (n : ℕ), 0 < B n) →
    (∀ (u : ℕ → α),
        (∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < B N) → ∃ x, Filter.Tendsto u Filter.atTop (nhds x)) →
      CompleteSpace α

A very useful criterion to show that a space is complete is to show that all sequences which satisfy a bound of the form dist (u n) (u m) < B N for all n m ≥ N are converging. This is often applied for B N = 2^{-N}, i.e., with a very fast convergence to 0, which makes it possible to use arguments of converging series, while this is impossible to do in general for arbitrary Cauchy sequences.

Defined in

Mathlib.Topology.MetricSpace.Cauchy

Cited by

2 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace