Theorems · Theorem · category theory

CategoryTheory.IsIso.inv_hom_id_assoc

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [I : CategoryTheory.IsIso f] {Z : C}
  (h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) (CategoryTheory.CategoryStruct.comp f h) = h

Defined in

Mathlib.CategoryTheory.Iso

Cited by

37 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.IsIso