naturality_comp

Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

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

Lean4

theorem naturality_comp {p f g h pf : C} {η : f ≅ g} {θ : g ≅ h} (η_f : p ⊗ f ≅ pf) (η_g : p ⊗ g ≅ pf)
    (η_h : p ⊗ h ≅ pf) (ih_η : p ◁ η ≪≫ η_g = η_f) (ih_θ : p ◁ θ ≪≫ η_h = η_g) : p ◁ (η ≪≫ θ) ≪≫ η_h = η_f := by
  simp_all

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

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

Разделы

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

Аффилиация

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