curriedActionMop_map_unmop_app

Mathlib.CategoryTheory.Monoidal.Action.End

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop_map_unmop_app

Lean4

@[simp]
theorem curriedActionMop_map_unmop_app {c c' : C} (f : c ⟶ c') (d : D) :
    ((curriedActionMop C D).map f).unmop.app d = f ⊵ₗ d :=
  rfl

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

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

Разделы

Аффилиация

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