Theorems · Definition · category theory

CategoryTheory.IsCardinalLocallyPresentable.casesOn

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {κ : Cardinal.{w}} →
      [inst_1 : Fact κ.IsRegular] →
        {motive : CategoryTheory.IsCardinalLocallyPresentable C κ → Sort u_1} →
          (t : CategoryTheory.IsCardinalLocallyPresentable C κ) →
            ([toHasCardinalFilteredGenerator : CategoryTheory.HasCardinalFilteredGenerator C κ] →
                [toHasColimitsOfSize : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C] → motive ⋯) →
              motive t

Defined in

Mathlib.CategoryTheory.Presentable.LocallyPresentable

Cited by

0 results in Mathlib

Foundations

Depth 23 from the axioms · uses Quot.sound

Assumes

CategoryTheory.CategoryFact