Theorems · Theorem · category theory

CategoryTheory.FinCategory.asTypeToObjAsType_map

∀ (α : Type u_1) [inst : Fintype α] [inst_1 : CategoryTheory.SmallCategory α] [inst_2 : CategoryTheory.FinCategory α]
  {x x_1 : CategoryTheory.FinCategory.AsType α} (a : Fin (Fintype.card (x ⟶ x_1))),
  (CategoryTheory.FinCategory.asTypeToObjAsType α).map a = (Fintype.equivFin (x ⟶ x_1)).symm a

Defined in

Mathlib.CategoryTheory.FinCategory.AsType

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeCategoryTheory.SmallCategoryCategoryTheory.FinCategory