Theorems · Definition · category theory

CategoryTheory.MorphismProperty.multiplicativeClosure.below.casesOn

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C}
  {motive : ⦃X Y : C⦄ → (x : X ⟶ Y) → W.multiplicativeClosure x → Prop}
  {motive_1 :
    {X Y : C} →
      {x : X ⟶ Y} →
        (t : W.multiplicativeClosure x) → CategoryTheory.MorphismProperty.multiplicativeClosure.below t → Prop}
  {X Y : C} {x : X ⟶ Y} {t : W.multiplicativeClosure x}
  (t_1 : CategoryTheory.MorphismProperty.multiplicativeClosure.below t),
  (∀ {x y : C} (f : x ⟶ y) (hf : W f), motive_1 ⋯ ⋯) →
    (∀ (x : C), motive_1 ⋯ ⋯) →
      (∀ {x y z : C} (f : x ⟶ y) (g : y ⟶ z) (hf : W.multiplicativeClosure f) (hg : W g)
          (ih : CategoryTheory.MorphismProperty.multiplicativeClosure.below hf) (hf_ih : motive f hf), motive_1 ⋯ ⋯) →
        motive_1 t t_1

Defined in

Mathlib.CategoryTheory.MorphismProperty.Composition

Cited by

0 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

CategoryTheory.Category