whiskerLeft_app

Mathlib.CategoryTheory.Category.Cat

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

Lean4

@[simp]
theorem whiskerLeft_app {C D E : Cat} (F : C ⟶ D) {G H : D ⟶ E} (η : G ⟶ H) (X : C) : (F ◁ η).app X = η.app (F.obj X) :=
  rfl

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

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

Разделы

Аффилиация

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