map_map

Mathlib.ModelTheory.Substructures

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Substructure.map_map

English

Mapping by g after f equals mapping by g ∘ f.

Русский

Отображение через g после f равно отображению через g ∘ f.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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