map_comp_eq

Mathlib.Topology.Category.TopCat.Opens

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.Opens.map_comp_eq

English

Equality of functors: map(f ≫ g) equals map g ⋙ map f.

Русский

Равенство функторов: map(f ≫ g) = map g ⋙ map f.

LaTeX

$$$\\mathrm{map}(f\\circ g) = \\mathrm{map}(g) \\circ \\mathrm{map}(f)$$$

Lean4

theorem map_comp_eq (f : X ⟶ Y) (g : Y ⟶ Z) : map (f ≫ g) = map g ⋙ map f :=
  rfl

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

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

Разделы

Аффилиация

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