congr_app

Mathlib.CategoryTheory.Functor.Category

URI: https://scilib.ai/kg/mathlib#CategoryTheory.NatTrans.congr_app

English

If α = β are natural transformations F ⟶ G, then for any X, α.app X = β.app X.

Русский

Если α = β — натуральные преобразования F ⟶ G, тогда для любого объекта X имеем α.app X = β.app X.

LaTeX

$$$ \alpha = \beta \quad \Rightarrow \quad \alpha.app X = \beta.app X. $$$

Lean4

theorem congr_app {α β : F ⟶ G} (h : α = β) (X : C) : α.app X = β.app X := by rw [h]

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

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

Разделы

Аффилиация

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