Theorems · Theorem · category theory

TopCat.range_prod_map

∀ {W X Y Z : TopCat} (f : W ⟶ Y) (g : X ⟶ Z),
  Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.map f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.fst) ⁻¹'
        Set.range ⇑(CategoryTheory.ConcreteCategory.hom f) ∩
      ⇑(CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.snd) ⁻¹'
        Set.range ⇑(CategoryTheory.ConcreteCategory.hom g)

Defined in

Mathlib.Topology.Category.TopCat.Limits.Products

Cited by

0 results in Mathlib

Foundations

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