Theorems · Definition · category theory

TopCat.partialSections

{J : Type u} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J TopCat) →
      {G : Finset J} → Finset (TopCat.FiniteDiagramArrow✝ G) → Set ((j : J) → ↑(F.obj j))

Partial sections of a cofiltered limit are sections when restricted to a finite subset of objects and morphisms of J.

Defined in

Mathlib.Topology.Category.TopCat.Limits.Konig

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategory