Theorems · Theorem · category theory

CategoryTheory.InducedWideCategory.Hom.mk.inj

∀ {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}
  {hom : F X ⟶ F Y} {property : P hom} {hom_1 : F X ⟶ F Y} {property_1 : P hom_1},
  { hom := hom, property := property } = { hom := hom_1, property := property_1 } → hom = hom_1

Defined in

Mathlib.CategoryTheory.Widesubcategory

Cited by

1 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms