Theorems · Theorem · category theory
CompHausLike.pullback.lift.congr_simp
∀ {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [inst : CompHausLike.HasExplicitPullback f g]
{Z : CompHausLike P} (a a_1 : Z ⟶ X) (e_a : a = a_1) (b b_1 : Z ⟶ Y) (e_b : b = b_1)
(w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g),
CompHausLike.pullback.lift f g a b w = CompHausLike.pullback.lift f g a_1 b_1 ⋯- Cited by
- 0 results in Mathlib
- Foundations
- Depth 95 from the axioms · uses propext, Classical.choice, 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.
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.CategoryStruct.compstatement and proof · cited by 17,999
- TopCatstatement and proof · cited by 1,889
- CompHausLikestatement and proof · cited by 145
- CompHausLike.HasExplicitPullbackstatement and proof · cited by 14
- CompHausLike.pullbackstatement · cited by 13
- CompHausLike.pullback.liftstatement and proof · cited by 6
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.