Theorems · Definition · category theory
compHausToTop
CategoryTheory.Functor CompHaus TopCat
The fully faithful embedding of CompHaus in TopCat.
- Defined in
- Mathlib.Topology.Category.CompHaus.Basic
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Functorstatement · cited by 16,252
- TopCatstatement and proof · cited by 1,889
- CompHausstatement · cited by 61
- CompHausLike.compHausLikeToTopproof · cited by 10
Cited by4
Results whose statement or proof uses this declaration.
- stoneCechEquivalencestatement and proof · cited by 0
- CompHaus.limitConeproof · cited by 0
- CompHaus.limitConeIsLimitproof · cited by 0
- Stonean.stoneCechEquivalenceproof · cited by 0