Theorems · Definition · category theory
UniformSpaceCat.completionHom
(X : UniformSpaceCat) → X ⟶ (CategoryTheory.forget₂ CpltSepUniformSpace UniformSpaceCat).obj (UniformSpaceCat.completionFunctor.obj X)
The inclusion of a uniform space into its completion.
- Defined in
- Mathlib.Topology.Category.UniformSpace
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement · cited by 32,603
- CategoryTheory.Functor.objstatement · cited by 19,642
- UniformContinuousstatement · cited by 410
- CategoryTheory.forget₂statement · cited by 260
- UniformSpace.Completion.coe'proof · cited by 144
- UniformSpaceCatstatement and proof · cited by 20
- UniformSpaceCat.carrierstatement · cited by 20
- CpltSepUniformSpacestatement · cited by 9
- CpltSepUniformSpace.αstatement · cited by 7
- UniformSpaceCat.completionFunctorstatement · cited by 4
Cited by3
Results whose statement or proof uses this declaration.
- UniformSpaceCat.extension_comp_homstatement · cited by 0
- UniformSpaceCat.adjproof · cited by 0
- UniformSpaceCat.completionHom_valstatement · cited by 0