Theorems · Theorem · category theory

CategoryTheory.initiallySmall_of_small_weakly_initial_set

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

Defined in

Mathlib.CategoryTheory.Limits.FinallySmall

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.IsCofilteredOrEmptySmall