Theorems · Theorem · category theory

CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.essentiallySmall_isPresentable

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {κ : Cardinal.{w}}
  [inst_1 : Fact κ.IsRegular],
  P.IsCardinalFilteredGenerator κ →
    ∀ [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.LocallySmall.{w, v, u} C],
      CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} (CategoryTheory.isCardinalPresentable C κ)

Defined in

Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFactCategoryTheory.ObjectProperty.EssentiallySmallCategoryTheory.LocallySmall