map_map

Mathlib.Algebra.Group.Subsemigroup.Operations

URI: https://scilib.ai/kg/mathlib#Subsemigroup.map_map

English

Imaging via successive maps commutes with composition: map g after map f equals map (g ∘ f).

Русский

Образ через последовательные отображения складывается: map g после map f равно map (g ∘ f).

LaTeX

$$$(S.map f).map g = S.map (g \\circ f)$$$

Lean4

@[to_additive]
theorem map_map (g : N →ₙ* P) (f : M →ₙ* N) : (S.map f).map g = S.map (g.comp f) :=
  SetLike.coe_injective <| image_image _ _ _

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

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

Разделы

Аффилиация

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