curry_natural_left — Mathlib

English

The equality in the hom-equivalence corresponds to equality under the equivalence; i.e., applying the homEquiv yields equality if and only if the underlying morphisms are equal.

Русский

Равенство в гом-эквивариантности соответствует равенству под эквивалентностью; то есть применение homEquiv сохраняет равенство и обратное.

LaTeX

$$$\mathrm{homEquiv}\_\mathrm{apply}\_eq(f,g) \iff f = g$$$

Lean4

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

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