uncurry_natural_right — Mathlib

English

Uncurry satisfies naturality on the right with respect to a map g: Y → Y': uncurry(f ≫ (ihom A).map g) = uncurry f ≫ g.

Русский

Uncurry удовлетворяет естественности справа по отношению к отображению g: uncurry(f ≫ (ihom A).map g) = uncurry f ≫ g.

LaTeX

$$$\mathrm{uncurry}(f \;\circ\; (\mathrm{ihom}(A)).map(g)) = \mathrm{uncurry}(f) \;\circ\; g$$$

Lean4

@[reassoc]
theorem uncurry_natural_right (f : X ⟶ A ⟶[C] Y) (g : Y ⟶ Y') : uncurry (f ≫ (ihom _).map g) = uncurry f ≫ g :=
  Adjunction.homEquiv_naturality_right_symm _ _ _

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