Theorems · Theorem · category theory

CategoryTheory.initiallySmall_iff_exists_small_weakly_initial_set

∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] [CategoryTheory.IsCofilteredOrEmpty J],
  CategoryTheory.InitiallySmall J ↔ ∃ s, ∃ (_ : Small.{v, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)

Defined in

Mathlib.CategoryTheory.Limits.FinallySmall

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.IsCofilteredOrEmpty