evalWhiskerRight_id

Mathlib.Tactic.CategoryTheory.Bicategory.Normalize

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

Lean4

theorem evalWhiskerRight_id {η : f ⟶ g} {η₁ : f ⟶ g ≫ 𝟙 b} {η₂ : f ≫ 𝟙 b ⟶ g ≫ 𝟙 b} (e_η₁ : η ≫ (ρ_ _).inv = η₁)
    (e_η₂ : (ρ_ _).hom ≫ η₁ = η₂) : η ▷ 𝟙 b = η₂ := by simp [e_η₁, e_η₂]

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

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

Разделы

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

Аффилиация

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