evalWhiskerRight_cons_of_of

Mathlib.Tactic.CategoryTheory.Bicategory.Normalize

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

Lean4

theorem evalWhiskerRight_cons_of_of {f g h i : a ⟶ b} {j : b ⟶ c} {α : f ≅ g} {η : g ⟶ h} {ηs : h ⟶ i}
    {ηs₁ : h ≫ j ⟶ i ≫ j} {η₁ : g ≫ j ⟶ h ≫ j} {η₂ : g ≫ j ⟶ i ≫ j} {η₃ : f ≫ j ⟶ i ≫ j} (e_ηs₁ : ηs ▷ j = ηs₁)
    (e_η₁ : η ▷ j = η₁) (e_η₂ : η₁ ≫ ηs₁ = η₂) (e_η₃ : (whiskerRightIso α j).hom ≫ η₂ = η₃) :
    (α.hom ≫ η ≫ ηs) ▷ j = η₃ := by simp_all

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

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

Разделы

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

Аффилиация

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