Theorems · Inductive type · general topology
CompleteSpace
(α : Type u) → [UniformSpace α] → Prop
A complete space is defined here using uniformities. A uniform space is complete if every Cauchy filter converges.
- Defined in
- Mathlib.Topology.UniformSpace.Cauchy
- Cited by
- 2,532 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- UniformSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- UniformSpacestatement · cited by 2,040
Cited by2,757
Results whose statement or proof uses this declaration.
- ContinuousLinearMap.adjointstatement and proof · cited by 82
- MeasureTheory.setToFunproof · cited by 77
- MeasureTheory.integral_conststatement and proof · cited by 75
- InnerProductSpace.toDualstatement and proof · cited by 45
- ImplicitFunctionDatastatement · cited by 44
- MeasureTheory.L1.setToL1statement and proof · cited by 44
- LinearMap.toContinuousLinearMapstatement and proof · cited by 43
- MeasureTheory.integral_defstatement and proof · cited by 41
- Summable.of_normstatement and proof · cited by 40
- MeasureTheory.condExpL2statement and proof · cited by 36
- intervalIntegral.integral_conststatement and proof · cited by 33
- ContinuousLinearMap.integral_comp_commstatement and proof · cited by 33
Showing the 200 most cited of 2,757.