Theorems · Definition · general topology

LightProfinite.limitCone

{J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.CountableCategory J] → (F : CategoryTheory.Functor J LightProfinite) → CategoryTheory.Limits.Cone F

An explicit limit cone for a functor F : J ⥤ LightProfinite, for a countable category J defined in terms of CompHaus.limitCone, which is defined in terms of TopCat.limitCone.

Defined in

Mathlib.Topology.Category.LightProfinite.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategoryCategoryTheory.CountableCategory