congr_map

Mathlib.CategoryTheory.Functor.Basic

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

English

If f = g, then F.map f = F.map g for any functor F : C ⥤ D.

Русский

Если f = g, то для любого функторa F : C ⥤ D выполняется F.map f = F.map g.

LaTeX

$$$ f = g \quad \Rightarrow \quad F.map f = F.map g. $$$

Lean4

theorem congr_map (F : C ⥤ D) {X Y : C} {f g : X ⟶ Y} (h : f = g) : F.map f = F.map g := by rw [h]

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

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

Разделы

Аффилиация

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