eq_mkNatTrans — Mathlib

English

The mkNatTrans built from the whiskered left and right parts equals α when tested against both sides.

Русский

Построенное через mkNatTrans из ослаблений слева и справа преобразование эквивалентно α на обе стороны.

LaTeX

$$$ mkNatTrans (whiskerLeft (inclLeft C D) α) (whiskerLeft (inclRight C D) α) = α $$$

Lean4

theorem eq_mkNatTrans {F F' : C ⋆ D ⥤ E} (α : F ⟶ F') :
    mkNatTrans (whiskerLeft (inclLeft C D) α) (whiskerLeft (inclRight C D) α) = α := by apply natTrans_ext <;> simp

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