Theorems · Definition · category theory

CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.casesOn

{J : Type w} →
  [inst : CategoryTheory.SmallCategory J] →
    {κ : Cardinal.{w}} →
      {motive : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ → Sort u} →
        (t : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ) →
          ((W : CategoryTheory.MorphismProperty J) →
              (P : CategoryTheory.ObjectProperty J) →
                (src : ∀ {i j : J} {f : i ⟶ j}, W f → P i) →
                  (tgt : ∀ {i j : J} {f : i ⟶ j}, W f → P j) →
                    (hW : W.HasCardinalLT κ) →
                      (hP : P.HasCardinalLT κ) →
                        motive { W := W, P := P, src := src, tgt := tgt, hW := hW, hP := hP }) →
            motive t

Defined in

Mathlib.CategoryTheory.Presentable.Directed

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategory