limit_π_homDiagram_eqToHom — Mathlib

English

The currying isomorphism between Cat.of (C ⥤ D ⥤ E) and Cat.of (C × D ⥤ E).

Русский

Изоморфия каррирования между Cat.of (C ⥤ D ⥤ E) и Cat.of (C × D ⥤ E).

LaTeX

$$$$\\mathrm{Iso}(\\mathrm{Cat.of}(\\mathrm{Functor}(C,\\mathrm{Functor}(D,E))), \\mathrm{Cat.of}(\\mathrm{Functor}(\\mathrm{Prod}(C,D), E))).$$$$

Lean4

@[simp]
theorem limit_π_homDiagram_eqToHom {F : J ⥤ Cat.{v, v}} (X Y : limit (F ⋙ Cat.objects.{v, v})) (j : J) (h : X = Y) :
    limit.π (homDiagram X Y) j (eqToHom h) = eqToHom (congr_arg (limit.π (F ⋙ Cat.objects.{v, v}) j) h) :=
  by
  subst h
  simp

Похожие утверждения