leftDerivedNatTrans_app — Mathlib

English

The app-component of leftDerivedNatTrans commutes with α and τ at a point X.

Русский

Компонента приложения leftDerivedNatTrans commute с α и τ на точке X.

LaTeX

$$$$ (leftDerivedNatTrans\\; LF'\\; LF\\; α'\\; α\\; W\\; τ).app (L.obj X) \\circ α.app X = α'.app X \\circ τ.app X. $$$$

Lean4

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

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