evalWhiskerLeft_id

Mathlib.Tactic.CategoryTheory.Bicategory.Normalize

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

Lean4

theorem evalWhiskerLeft_id {η : f ⟶ g} {η₁ : f ⟶ 𝟙 a ≫ g} {η₂ : 𝟙 a ≫ f ⟶ 𝟙 a ≫ g} (e_η₁ : η ≫ (λ_ _).inv = η₁)
    (e_η₂ : (λ_ _).hom ≫ η₁ = η₂) : 𝟙 a ◁ η = η₂ := by simp [e_η₁, e_η₂]

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

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

Разделы

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

Аффилиация

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