Theorems · Theorem · category theory

CategoryTheory.ObjectProperty.EssentiallySmall.of_functor

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D),
  CategoryTheory.ObjectProperty.EssentiallySmall.{w, v', u'} (P.map F) →
    (∀ (Y : D), CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} (P ⊓ fun x => Nonempty (F.obj x ≅ Y))) →
      CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P

Defined in

Mathlib.CategoryTheory.ObjectProperty.Small

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category