pre_id

Mathlib.CategoryTheory.Closed.Monoidal

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

English

Equivalence between equality of curry f and g and equality of f and uncurry g.

Русский

Эквивалентность: равенство curry f и g ↔ равенство f и uncurry g.

LaTeX

$$$\mathrm{Eq}$ (Eq)\big(\mathrm{curry} f, g\big) \;\iff\; \mathrm{Eq}(\mathrm{uncurry} g, f)$$$

Lean4

@[simp]
theorem pre_id (A : C) [Closed A] : pre (𝟙 A) = 𝟙 _ :=
  by
  rw [pre, Functor.map_id]
  apply conjugateEquiv_id

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

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

Разделы

Аффилиация

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