Theorems · Theorem · category theory

CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.essentiallyLarge_top

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

Defined in

Mathlib.CategoryTheory.Presentable.EssentiallyLarge

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFactCategoryTheory.LocallySmallCategoryTheory.ObjectProperty.EssentiallySmall