Theorems · Theorem · category theory

CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.hasCardinalFilteredGenerator

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

Defined in: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Cited by: 0 results in Mathlib
Foundations: Depth 22 from the axioms · uses Quot.sound
Assumes: CategoryTheory.Category CategoryTheory.ObjectProperty.EssentiallySmall CategoryTheory.LocallySmall Fact

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
Factstatement and proof · cited by 2,726
Cardinalstatement and proof · cited by 2,598
CategoryTheory.ObjectPropertystatement and proof · cited by 798
Cardinal.IsRegularstatement and proof · cited by 282
CategoryTheory.LocallySmallstatement and proof · cited by 242
CategoryTheory.ObjectProperty.EssentiallySmallstatement and proof · cited by 26
CategoryTheory.ObjectProperty.IsCardinalFilteredGeneratorstatement and proof · cited by 22
CategoryTheory.HasCardinalFilteredGeneratorstatement · cited by 9

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.