Theorems · Definition · category theory

CategoryTheory.HomRel.IsStableUnderPostcomp.casesOn

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {r : HomRel C} →
      {motive : CategoryTheory.HomRel.IsStableUnderPostcomp r → Sort u} →
        (t : CategoryTheory.HomRel.IsStableUnderPostcomp r) →
          ((comp_right :
                ∀ {X Y Z : C} {f f' : X ⟶ Y} (g : Y ⟶ Z),
                  r f f' → r (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f' g)) →
              motive ⋯) →
            motive t

Defined in

Mathlib.CategoryTheory.Quotient

Cited by

0 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CategoryTheory.Category