evalWhiskerLeft_of_cons

Mathlib.Tactic.CategoryTheory.Bicategory.Normalize

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

Lean4

theorem evalWhiskerLeft_of_cons {f : a ⟶ b} {g h i j : b ⟶ c} (α : g ≅ h) (η : h ⟶ i) {ηs : i ⟶ j} {θ : f ≫ i ⟶ f ≫ j}
    (e_θ : f ◁ ηs = θ) : f ◁ (α.hom ≫ η ≫ ηs) = (whiskerLeftIso f α).hom ≫ f ◁ η ≫ θ := by simp [e_θ]

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

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

Разделы

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

Аффилиация

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