Theorems · Theorem · category theory

TopCat.partialSections.nonempty

∀ {J : Type u} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCat)
  [CategoryTheory.IsCofilteredOrEmpty J] [h : ∀ (j : J), Nonempty ↑(F.obj j)] {G : Finset J}
  (H : Finset (TopCat.FiniteDiagramArrow✝ G)), (TopCat.partialSections F H).Nonempty

Defined in

Mathlib.Topology.Category.TopCat.Limits.Konig

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategoryCategoryTheory.IsCofilteredOrEmptyNonempty