StructuralOfExpr_monoidalComp

Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Monoidal.StructuralOfExpr_monoidalComp

Lean4

theorem StructuralOfExpr_monoidalComp {f g h i : C} [MonoidalCoherence g h] (η : f ⟶ g) (η' : f ≅ g) (ih_η : η'.hom = η)
    (θ : h ⟶ i) (θ' : h ≅ i) (ih_θ : θ'.hom = θ) : (η' ≪⊗≫ θ').hom = η ⊗≫ θ := by
  simp [ih_η, ih_θ, monoidalIsoComp, monoidalComp]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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