Theorems · Theorem · category theory

CategoryTheory.InducedCategory.isoMk_inv

∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v, u₂} D] {F : C → D}
  {X Y : CategoryTheory.InducedCategory D F} (f : F X ≅ F Y),
  (CategoryTheory.InducedCategory.isoMk f).inv = CategoryTheory.InducedCategory.homMk f.inv

Defined in

Mathlib.CategoryTheory.InducedCategory

Cited by

0 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext

Assumes

CategoryTheory.Category