curryingFlipEquiv — Mathlib

English

The flipped currying equivalence, relating D ⥤ C ⥤ E and C ⥤ D ⥤ E

Русский

Перевёрнутая эквивалентность каррирования связывает D ⥤ C ⥤ E и C ⥤ D ⥤ E

LaTeX

$$$\text{curryingFlipEquiv} : D \! \to \! C \! \to E \simeq C \! \to \! D \! \to E$$$

Lean4

/-- The flipped equivalence of types of bifunctors given by currying. -/
@[simps!]
def curryingFlipEquiv : D ⥤ C ⥤ E ≃ C × D ⥤ E :=
  flippingEquiv.trans curryingEquiv

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