pre_comm_ihom_map — Mathlib

English

Uncurrying the identity on A ⟶ X yields evaluation morphism with A substituted for B.

Русский

Развёртывая тождество на A ⟶ X, получаем оценку с A вместо B.

LaTeX

$$$\mathrm{uncurry}(\mathrm{id}_{A \to X}) = (\mathrm{ihom.ev} A).app X$$$

Lean4

theorem pre_comm_ihom_map {W X Y Z : C} [Closed W] [Closed X] (f : W ⟶ X) (g : Y ⟶ Z) :
    (pre f).app Y ≫ (ihom W).map g = (ihom X).map g ≫ (pre f).app Z := by simp

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