Theorems · Definition · general topology
profiniteToCompHaus
CategoryTheory.Functor Profinite CompHaus
The fully faithful embedding of Profinite in CompHaus.
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 29 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Functorstatement · cited by 16,252
- TopCat.carrierstatement and proof · cited by 3,184
- TopCatstatement and proof · cited by 1,889
- TotallyDisconnectedSpacestatement and proof · cited by 295
- Profinitestatement · cited by 75
- CompHausstatement · cited by 61
- compHausLikeToCompHausproof · cited by 0
Cited by16
Results whose statement or proof uses this declaration.
- Condensed.ProfiniteCompHaus.equivalencestatement and proof · cited by 4
- CondensedSet.isDiscrete_tfaestatement and proof · cited by 1
- CondensedSet.mem_locallyConstant_essImage_of_isColimit_mapCoconestatement and proof · cited by 1
- Profinite.limitConeproof · cited by 1
- Profinite.effectiveEpiFamily_tfaeproof · cited by 1
- Condensed.isSheafProfinitestatement and proof · cited by 0
- Condensed.ofSheafForgetProfinitestatement and proof · cited by 0
- Condensed.ofSheafProfinitestatement and proof · cited by 0
- Profinite.limitConeIsLimitproof · cited by 0
- Profinite.presentationproof · cited by 0
- Profinite.profiniteToCompHausEffectivePresentationstatement · cited by 0
- Profinite.toCompHausEquivalencestatement and proof · cited by 0