evalWhiskerLeft_comp

Mathlib.Tactic.CategoryTheory.Bicategory.Normalize

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

Lean4

theorem evalWhiskerLeft_comp {f : a ⟶ b} {g : b ⟶ c} {h i : c ⟶ d} {η : h ⟶ i} {η₁ : g ≫ h ⟶ g ≫ i}
    {η₂ : f ≫ g ≫ h ⟶ f ≫ g ≫ i} {η₃ : f ≫ g ≫ h ⟶ (f ≫ g) ≫ i} {η₄ : (f ≫ g) ≫ h ⟶ (f ≫ g) ≫ i} (e_η₁ : g ◁ η = η₁)
    (e_η₂ : f ◁ η₁ = η₂) (e_η₃ : η₂ ≫ (α_ _ _ _).inv = η₃) (e_η₄ : (α_ _ _ _).hom ≫ η₃ = η₄) : (f ≫ g) ◁ η = η₄ := by
  simp [e_η₁, e_η₂, e_η₃, e_η₄]

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

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

Разделы

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

Аффилиация

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