Theorems · Theorem · category theory

TopCat.pullback_fst_range

∀ {X Y S : TopCat} (f : X ⟶ S) (g : Y ⟶ S),
  Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g)) =
    {x | ∃ y, (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) y}

Defined in

Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Cited by

2 results in Mathlib

Foundations

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