Theorems · Theorem · category theory

CategoryTheory.Limits.productUniqueIso_inv

Deprecated since 2026-06-30Use CategoryTheory.Limits.productUniqueIso_inv_π instead.

∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : Unique β] (f : β → C) (b : β),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.productUniqueIso f).inv (CategoryTheory.Limits.Pi.π f b) =
    CategoryTheory.eqToHom ⋯

Alias of CategoryTheory.Limits.productUniqueIso_inv_π.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Products

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryUnique