congr_app — Mathlib

English

If two natural transformations α, β: F ⇒ G are equal (α = β), then their components at every object X are equal: α_X = β_X.

Русский

Пусть две естественные преобразования α, β: F ⇒ G равны; тогда их компоненты на каждом объекте X совпадают: α_X = β_X.

LaTeX

$$$\alpha_X = \beta_X$$$

Lean4

theorem congr_app {F G : C ⥤ D} {α β : NatTrans F G} (h : α = β) (X : C) : α.app X = β.app X := by cat_disch

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