congr_app

Mathlib.CategoryTheory.Functor.FunctorHom

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

Lean4

theorem congr_app {f g : HomObj F G A} (h : f = g) (X : C) (a : A.obj X) : f.app X a = g.app X a := by subst h; rfl

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

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

Разделы

Аффилиация

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