curry_natural_left — Mathlib

English

Curry is natural with respect to left whiskering: curry(◁ f ≫ g) = f ≫ curry(g).

Русский

Кэрри-образование естественно по слевамому клейку: curry(◁ f ≫ g) = f ≫ curry(g).

LaTeX

$$$\mathrm{curry}(\triangleleft f \;\lrcorner\; g) = f \;\gg\; \mathrm{curry}(g)$$$

Lean4

@[reassoc]
theorem curry_natural_left (f : X ⟶ X') (g : A ⊗ X' ⟶ Y) : curry (_ ◁ f ≫ g) = f ≫ curry g :=
  Adjunction.homEquiv_naturality_left _ _ _

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