Theorems · Theorem · category theory

TopCat.nonempty_isLimit_iff_eq_induced

∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat}
  (c : CategoryTheory.Limits.Cone F) (hc : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget TopCat).mapCone c)),
  Nonempty (CategoryTheory.Limits.IsLimit c) ↔
    c.pt.str = ⨅ j, TopologicalSpace.induced (⇑(CategoryTheory.ConcreteCategory.hom (c.π.app 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.Category