Theorems · Theorem · category theory

CategoryTheory.InitiallySmall.exists_of_isCofiltered

∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C]
  [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.InitiallySmall C],
  ∃ D x, ∃ (_ : CategoryTheory.IsCofiltered D), ∃ F, F.Initial

Defined in

Mathlib.CategoryTheory.Filtered.FinallySmall

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.IsCofilteredCategoryTheory.LocallySmallCategoryTheory.InitiallySmall