Theorems · Definition · category theory

CategoryTheory.HasCardinalFilteredGenerator.casesOn

{C : Type u} →
  [hC : CategoryTheory.Category.{v, u} C] →
    {κ : Cardinal.{w}} →
      [hκ : Fact κ.IsRegular] →
        {motive : CategoryTheory.HasCardinalFilteredGenerator C κ → Sort u_1} →
          (t : CategoryTheory.HasCardinalFilteredGenerator C κ) →
            ([toLocallySmall : CategoryTheory.LocallySmall.{w, v, u} C] →
                (exists_generator :
                    ∃ P,
                      ∃ (_ : CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P),
                        P.IsCardinalFilteredGenerator κ) →
                  motive ⋯) →
              motive t

Defined in

Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation

Cited by

0 results in Mathlib

Foundations

Depth 23 from the axioms · uses Quot.sound

Assumes

CategoryTheory.CategoryFact