Theorems · Theorem · category theory

CategoryTheory.Limits.StrongEpiMonoFactorisation.mk.inj

∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X ⟶ Y}
  {toMonoFactorisation : CategoryTheory.Limits.MonoFactorisation f}
  {e_strong_epi : CategoryTheory.StrongEpi toMonoFactorisation.e}
  {toMonoFactorisation_1 : CategoryTheory.Limits.MonoFactorisation f}
  {e_strong_epi_1 : CategoryTheory.StrongEpi toMonoFactorisation_1.e},
  { toMonoFactorisation := toMonoFactorisation, e_strong_epi := e_strong_epi } =
      { toMonoFactorisation := toMonoFactorisation_1, e_strong_epi := e_strong_epi_1 } →
    toMonoFactorisation = toMonoFactorisation_1

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Images

Cited by

1 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms