uncurryObjFlip — Mathlib

English

The uncurrying of F.flip is isomorphic to swapping the factors followed by the uncurrying of F.

Русский

Раскурривание F.flip изоморфно перестановке факторов после раскурривания F.

LaTeX

$$$\operatorname{uncurry.obj} Fflip \cong (\mathrm{Prod.swap}\, D\, C) \circ \operatorname{uncurry.obj} F$$$

Lean4

/-- The uncurrying of `F.flip` is isomorphic to
swapping the factors followed by the uncurrying of `F`. -/
@[simps!]
def uncurryObjFlip (F : C ⥤ D ⥤ E) : uncurry.obj F.flip ≅ Prod.swap _ _ ⋙ uncurry.obj F :=
  NatIso.ofComponents fun _ => Iso.refl _

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