Theorems · Theorem · category theory

TopCat.nonempty_limitCone_of_compact_t2_cofiltered_system

∀ {J : Type u} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCat)
  [CategoryTheory.IsCofilteredOrEmpty J] [∀ (j : J), Nonempty ↑(F.obj j)] [∀ (j : J), CompactSpace ↑(F.obj j)]
  [∀ (j : J), T2Space ↑(F.obj j)], Nonempty ↑(TopCat.limitCone F).pt

Cofiltered limits of nonempty compact Hausdorff spaces are nonempty topological spaces.

Defined in

Mathlib.Topology.Category.TopCat.Limits.Konig

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategoryCategoryTheory.IsCofilteredOrEmptyNonemptyCompactSpaceT2Space