Theorems · Theorem · category theory

CategoryTheory.InducedWideCategory.Hom.property

∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} D] {F : C → D}
  {P : CategoryTheory.MorphismProperty D} [inst_1 : P.IsMultiplicative] {X Y : CategoryTheory.InducedWideCategory D F P}
  (self : X.Hom Y), P self.hom

The property that the morphism satisfies.

Defined in

Mathlib.CategoryTheory.Widesubcategory

Cited by

0 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.IsMultiplicative