Theorems · Theorem · category theory

TopCat.colimit_isOpen_iff

∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J TopCat)
  [inst_1 : CategoryTheory.Limits.HasColimit F] (U : Set ↑(CategoryTheory.Limits.colimit F)),
  IsOpen U ↔ ∀ (j : J), IsOpen (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) ⁻¹' U)

Defined in

Mathlib.Topology.Category.TopCat.Limits.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasColimit