uncurry_pre

Mathlib.CategoryTheory.Closed.Monoidal

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MonoidalClosed.uncurry_pre

English

Uncurrying the identity on A ⟶[C] X gives the evaluation morphism at X.

Русский

Развёртывание тождества на A ⟶ X даёт морфизм оценки в X.

LaTeX

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

Lean4

@[simp]
theorem uncurry_pre (f : B ⟶ A) (X : C) : MonoidalClosed.uncurry ((pre f).app X) = f ▷ _ ≫ (ihom.ev A).app X := by
  simp [uncurry_eq]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru