Theorems · Definition · category theory
CompHausLike.pullback
{P : TopCat → Prop} →
{X Y B : CompHausLike P} → (f : X ⟶ B) → (g : Y ⟶ B) → [CompHausLike.HasExplicitPullback f g] → CompHausLike PThe pullback of two morphisms f,g in CompHaus, constructed explicitly as the set of
pairs (x,y) such that f x = g y, with the topology induced by the product.
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Quiver.Homstatement and proof · cited by 32,603
- Set.Elemproof · cited by 7,166
- Set.ofPredproof · cited by 6,101
- CategoryTheory.ConcreteCategory.homproof · cited by 4,022
- TopCat.carrierproof · cited by 3,184
- TopCatstatement and proof · cited by 1,889
- CompHausLike.toTopproof · cited by 258
- CompHausLikestatement and proof · cited by 145
- CompHausLike.ofproof · cited by 24
- CompHausLike.HasExplicitPullbackstatement and proof · cited by 14
Cited by16
Results whose statement or proof uses this declaration.
- CompHausLike.preregularproof · cited by 19
- CompHausLike.pullback.fststatement and proof · cited by 7
- CompHausLike.pullback.sndstatement and proof · cited by 7
- CompHausLike.pullback.liftstatement · cited by 6
- CompHausLike.pullback.conditionstatement and proof · cited by 3
- CompHausLike.pullback.lift_fststatement · cited by 1
- CompHausLike.pullback.lift_sndstatement · cited by 1
- CompHausLike.pullback.condition_assocstatement · cited by 0
- CompHausLike.pullback.cone_ptstatement · cited by 0
- CompHausLike.pullback.cone_πstatement · cited by 0
- CompHausLike.pullback.congr_simpstatement and proof · cited by 0
- CompHausLike.pullback.hom_extstatement and proof · cited by 0