rightDerivedNatTrans_app — Mathlib

English

For τ and X, the app component satisfies α.app X ≫ (rightDerivedNatTrans_RF_RF' α α' W τ).app (L.obj X) = τ.app X ≫ α'.app X.

Русский

Компонент приложения удовлетворяет: ...

LaTeX

$$[τ : F ⟶ F'] (X) : α.app X ≫ (rightDerivedNatTrans RF RF' α α' W τ).app (L.obj X) = τ.app X ≫ α'.app X$$

Lean4

@[reassoc (attr := simp)]
theorem rightDerivedNatTrans_app (τ : F ⟶ F') (X : C) :
    α.app X ≫ (rightDerivedNatTrans RF RF' α α' W τ).app (L.obj X) = τ.app X ≫ α'.app X :=
  by
  dsimp only [rightDerivedNatTrans]
  simp

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