Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.multiplicativeClosure.brecOn

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C}
  {motive : ⦃X Y : C⦄ → (x : X ⟶ Y) → W.multiplicativeClosure x → Prop} {X Y : C} {x : X ⟶ Y}
  (t : W.multiplicativeClosure x),
  (∀ ⦃X Y : C⦄ (x : X ⟶ Y) (t : W.multiplicativeClosure x),
      CategoryTheory.MorphismProperty.multiplicativeClosure.below t → motive x t) →
    motive x t

Defined in

Mathlib.CategoryTheory.MorphismProperty.Composition

Cited by

0 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CategoryTheory.Category