Theorems · Theorem · category theory

CategoryTheory.Limits.preservesFiniteLimits_of_preservesFiniteLimitsOfSize

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D),
  (∀ (J : Type w) {𝒥 : CategoryTheory.SmallCategory J} (x : CategoryTheory.FinCategory J),
      CategoryTheory.Limits.PreservesLimitsOfShape J F) →
    CategoryTheory.Limits.PreservesFiniteLimits F

We can always derive PreservesFiniteLimits C by showing that we are preserving limits at an arbitrary universe.

Defined in

Mathlib.CategoryTheory.Limits.Preserves.Finite

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category