Theorems · Theorem · category theory

CategoryTheory.IsIso.hom_inv_id_assoc

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

Defined in

Mathlib.CategoryTheory.Iso

Cited by

29 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.IsIso