Theorems · Theorem · category theory

TopCat.isOpenEmbedding_of_pullback

∀ {X Y S : TopCat} {f : X ⟶ S} {g : Y ⟶ S},
  Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f) →
    Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom g) →
      Topology.IsOpenEmbedding
        ⇑(CategoryTheory.ConcreteCategory.hom
            (CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.one))

If X ⟶ S, Y ⟶ S are open embeddings, then so is X ×ₛ Y ⟶ S.

Defined in

Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Cited by

0 results in Mathlib

Foundations

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