Theorems · Definition · category theory
TopPair.ofTopCat
TopCat → TopPair
Constructs the topological pair (X, ∅) from X : TopCat.
- Defined in
- Mathlib.Topology.Category.TopPair
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopCatstatement and proof · cited by 1,889
- CategoryTheory.Limits.IsInitial.toproof · cited by 119
- TopPairstatement · cited by 67
- TopCat.isInitialPEmptyproof · cited by 2
- TopPair.ofproof · cited by 0
Cited by9
Results whose statement or proof uses this declaration.
- TopPair.inclproof · cited by 28
- TopPair.HomologyPretheory.inv_hom_iso_homₚ_appstatement · cited by 1
- TopPair.HomologyPretheory.iso_homₚ_inv_hom_appstatement · cited by 1
- TopPair.HomologyPretheory.Hom.iso_comm_appstatement · cited by 1
- TopPair.HomologyPretheory.inv_hom_iso_homₚ_app_assocstatement and proof · cited by 0
- TopPair.incl_mapstatement · cited by 0
- TopPair.incl_objstatement · cited by 0
- TopPair.HomologyPretheory.iso_homₚ_inv_hom_app_assocstatement and proof · cited by 0
- TopPair.HomologyPretheory.Hom.iso_comm_app_assocstatement and proof · cited by 0