Theorems · Definition · general topology
IsComplete
{α : Type u} → [uniformSpace : UniformSpace α] → Set α → PropA 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).
- Defined in
- Mathlib.Topology.UniformSpace.Cauchy
- Cited by
- 68 results in Mathlib
- Foundations
- Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- UniformSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Filterproof · cited by 8,121
- nhdsproof · cited by 5,554
- UniformSpacestatement and proof · cited by 2,040
- Filter.principalproof · cited by 740
- Cauchyproof · cited by 115
Cited by71
Results whose statement or proof uses this declaration.
- IsClosed.isCompletestatement · cited by 19
- completeSpace_iff_isComplete_rangestatement and proof · cited by 11
- ContractingWith.efixedPoint'statement and proof · cited by 7
- IsUniformInducing.completeSpace_congrproof · cited by 6
- completeSpace_coe_iff_isCompletestatement and proof · cited by 6
- IsComplete.isClosedstatement and proof · cited by 6
- isCompact_iff_totallyBounded_isCompletestatement and proof · cited by 6
- isComplete_image_iffstatement · cited by 5
- isComplete_univstatement · cited by 5
- completeSpace_iff_isComplete_univstatement · cited by 5
- cauchySeq_tendsto_of_isCompletestatement and proof · cited by 5
- IsUniformInducing.isComplete_rangestatement · cited by 4