Theorems · Theorem · category theory

CategoryTheory.Subobject.le_of_comm

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B : C} {X Y : CategoryTheory.Subobject B}
  (f : CategoryTheory.Subobject.underlying.obj X ⟶ CategoryTheory.Subobject.underlying.obj Y),
  CategoryTheory.CategoryStruct.comp f Y.arrow = X.arrow → X ≤ Y

Defined in

Mathlib.CategoryTheory.Subobject.Basic

Cited by

10 results in Mathlib

Foundations

Depth 40 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category