uncurry_ihom_map — Mathlib

English

A variant of uncurry(ihom A).map g equals (ihom.ev A).app Y composed with g.

Русский

Вариант развёртывания ihom A. map g равен композиции ev A в точке Y с g.

LaTeX

$$$\mathrm{uncurry}\big((\mathrm{ihom} A).\mathrm{map} g\big) = (\mathrm{ihom.ev} A).app Y \circ g$$$

Lean4

theorem uncurry_ihom_map (g : Y ⟶ Y') : uncurry ((ihom A).map g) = (ihom.ev A).app Y ≫ g :=
  by
  apply curry_injective
  rw [curry_uncurry, curry_natural_right, ← uncurry_id_eq_ev, curry_uncurry, id_comp]

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