Theorems · Theorem · general topology
CompleteSpace.complete
∀ {α : Type u} {inst : UniformSpace α} [self : CompleteSpace α] {f : Filter α}, Cauchy f → ∃ x, f ≤ nhds xIn a complete uniform space, every Cauchy filter converges.
- Defined in
- Mathlib.Topology.UniformSpace.Cauchy
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CompleteSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Filterstatement · cited by 8,121
- nhdsstatement · cited by 5,554
- CompleteSpacestatement and proof · cited by 2,532
- UniformSpacestatement and proof · cited by 2,040
- Cauchystatement · cited by 115
Cited by19
Results whose statement or proof uses this declaration.
- IsClosed.isCompleteproof · cited by 19
- cauchySeq_tendsto_of_completeproof · cited by 10
- isComplete_univproof · cited by 5
- multipliable_one_add_of_summableproof · cited by 4
- cauchy_iff_exists_le_nhdsproof · cited by 3
- uniformly_extend_existsproof · cited by 3
- Cauchy.le_nhds_limproof · cited by 2
- NonarchimedeanAddGroup.summable_of_tendsto_cofinite_zeroproof · cited by 2
- BoundedVariationOn.exists_tendsto_left_of_filterproof · cited by 2
- IsAdic.isPrecomplete_iffproof · cited by 2
- CompleteSpace.fst_of_prodproof · cited by 2
- IsDenseInducing.continuous_extend_of_cauchyproof · cited by 1