whiskerLeft_curry_ihom_ev_app — Mathlib

English

Uncurrying the image of a map g under ihom A yields the composition of ev A and g.

Русский

Развёртывая образ отображения g через ihom A, получаем состав ev A и g.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem whiskerLeft_curry_ihom_ev_app (g : A ⊗ Y ⟶ X) : A ◁ curry g ≫ (ihom.ev A).app X = g := by simp [curry_eq]

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