Theorems · Theorem · category theory

CategoryTheory.Limits.Types.exists_of_isPullback

∀ {X₁ X₂ X₃ X₄ : Type u} {t : X₁ ⟶ X₂} {r : X₂ ⟶ X₄} {l : X₁ ⟶ X₃} {b : X₃ ⟶ X₄},
  CategoryTheory.IsPullback t l r b →
    ∀ (x₂ : X₂) (x₃ : X₃),
      (CategoryTheory.ConcreteCategory.hom r) x₂ = (CategoryTheory.ConcreteCategory.hom b) x₃ →
        ∃ x₁, (CategoryTheory.ConcreteCategory.hom t) x₁ = x₂ ∧ (CategoryTheory.ConcreteCategory.hom l) x₁ = x₃

Defined in: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Cited by: 2 results in Mathlib
Foundations: Depth 33 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites10

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

DFunLike.coestatement and proof · cited by 62,936
Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.ConcreteCategory.homstatement and proof · cited by 4,022
TypeCat.Funstatement · cited by 1,307
CategoryTheory.Limits.Cone.ptproof · cited by 1,298
CategoryTheory.IsPullbackstatement and proof · cited by 320
Equiv.surjectiveproof · cited by 198
CategoryTheory.IsPullback.isLimitproof · cited by 47
CategoryTheory.IsPullback.coneproof · cited by 16
CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObjproof · cited by 7

Cited by2

Results whose statement or proof uses this declaration.

CategoryTheory.Limits.Types.isPullback_iffproof · cited by 4
CategoryTheory.Limits.Types.mono_of_isPushout_of_isPullbackproof · cited by 1