whiskerRight_app

Mathlib.CategoryTheory.Category.Cat

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

Lean4

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

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

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

Разделы

Аффилиация

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