ihom_obj

Mathlib.CategoryTheory.Category.Cat.CartesianClosed

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Cat.ihom_obj

Lean4

@[simp]
theorem ihom_obj (D : Type u) [Category.{u} D] : (ihom (Cat.of C)).obj (Cat.of D) = Cat.of (C ⥤ D) :=
  rfl

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

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

Разделы

Аффилиация

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