Theorems · Theorem · category theory

TopCat.limit_topology

∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J TopCat)
  [inst_1 : CategoryTheory.Limits.HasLimit F],
  (CategoryTheory.Limits.limit F).str =
    ⨅ j,
      TopologicalSpace.induced (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j)))
        (F.obj j).str

Defined in

Mathlib.Topology.Category.TopCat.Limits.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasLimit