Theorems · Theorem · category theory

CategoryTheory.Limits.MultispanIndex.map_fst

∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.Limits.MultispanShape}
  (d : CategoryTheory.Limits.MultispanIndex J C) (F : CategoryTheory.Functor C D) (i : J.L),
  (d.map F).fst i = F.map (d.fst i)

Defined in

Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

Cited by

0 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Category