Theorems · Definition · category theory

CompHausLike.pullback.isLimit

{P : TopCat → Prop} →
  {X Y B : CompHausLike P} →
    (f : X ⟶ B) →
      (g : Y ⟶ B) →
        [inst : CompHausLike.HasExplicitPullback f g] → CategoryTheory.Limits.IsLimit (CompHausLike.pullback.cone f g)

The explicit pullback cone is a limit cone.

Defined in: Mathlib.Topology.Category.CompHausLike.Limits
Cited by: 2 results in Mathlib
Foundations: Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CompHausLike.HasExplicitPullback

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Quiver.Homstatement and proof · cited by 32,603
TopCatstatement and proof · cited by 1,889
CategoryTheory.Limits.WalkingPairstatement · cited by 1,319
CategoryTheory.Limits.IsLimitstatement · cited by 664
CategoryTheory.Limits.WalkingCospanstatement · cited by 496
CategoryTheory.Limits.cospanstatement · cited by 467
CompHausLikestatement and proof · cited by 145
CategoryTheory.Limits.PullbackConeproof · cited by 136
CategoryTheory.Limits.PullbackCone.fstproof · cited by 118
CategoryTheory.Limits.PullbackCone.sndproof · cited by 113
CompHausLike.HasExplicitPullbackstatement and proof · cited by 14
CompHausLike.pullback.liftproof · cited by 6

Cited by2

Results whose statement or proof uses this declaration.

CompHausLike.pullback.isLimit_liftstatement and proof · cited by 0
LightCondensed.internallyProjective_free_natUnionInftyproof · cited by 0