curry_pre_app — Mathlib

English

Equality between curry f and g is equivalent to equality between f and uncurry g.

Русский

Равенство curry f и g эквивалентно равенству f и uncurry g.

LaTeX

$$$\mathrm{curry} f = g \iff \mathrm{uncurry} g = f$$$

Lean4

@[reassoc]
theorem curry_pre_app (f : B ⟶ A) {X Y : C} (g : A ⊗ Y ⟶ X) : curry g ≫ (pre f).app X = curry (f ▷ _ ≫ g) :=
  uncurry_injective
    (by
      rw [uncurry_curry, uncurry_eq, MonoidalCategory.whiskerLeft_comp, assoc, id_tensor_pre_app_comp_ev,
        whisker_exchange_assoc, whiskerLeft_curry_ihom_ev_app])

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