structuralIsoOfExpr_comp

Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Bicategory.structuralIsoOfExpr_comp

Lean4

theorem structuralIsoOfExpr_comp {f g h : a ⟶ b} (η : f ⟶ g) (η' : f ≅ g) (ih_η : η'.hom = η) (θ : g ⟶ h) (θ' : g ≅ h)
    (ih_θ : θ'.hom = θ) : (η' ≪≫ θ').hom = η ≫ θ := by simp [ih_η, ih_θ]

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

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

Разделы

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

Аффилиация

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