Theorems · Theorem · category theory

TopCat.range_pullback_to_prod

∀ {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z),
  Set.range
      ⇑(CategoryTheory.ConcreteCategory.hom
          (CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.pullback.fst f g)
            (CategoryTheory.Limits.pullback.snd f g))) =
    {x |
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst f)) x =
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd g)) x}

Defined in

Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Cited by

0 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound