Theorems · Definition · category theory

CategoryTheory.Limits.ChosenEndsOfShape.casesOn

{J : Type u_3} →
  [inst : CategoryTheory.Category.{v_3, u_3} J] →
    {C : Type u_4} →
      [inst_1 : CategoryTheory.Category.{v_4, u_4} C] →
        {motive : CategoryTheory.Limits.ChosenEndsOfShape J C → Sort u} →
          (t : CategoryTheory.Limits.ChosenEndsOfShape J C) →
            ((wedge : (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) → CategoryTheory.Limits.Wedge F) →
                (isEnd :
                    (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) →
                      CategoryTheory.Limits.IsLimit (wedge F)) →
                  motive { wedge := wedge, isEnd := isEnd }) →
              motive t

Defined in

Mathlib.CategoryTheory.Limits.Chosen.End

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category