map_comp_map — Mathlib

English

The coproduct map preserves composition: map(f', g') ∘ map(f, g) = map(f' ∘ f, g' ∘ g).

Русский

Отображение копрода сохраняет композицию: map(f', g') ∘ map(f, g) = map(f' ∘ f, g' ∘ g).

LaTeX

$$$ (\operatorname{map}(f',g')) \circ (\operatorname{map}(f,g)) = \operatorname{map}(f' \circ f, g' \circ g) $$$$

Lean4

@[to_additive]
theorem map_comp_map {M'' N''} [MulOneClass M''] [MulOneClass N''] (f' : M' →* M'') (g' : N' →* N'') (f : M →* M')
    (g : N →* N') : (map f' g').comp (map f g) = map (f'.comp f) (g'.comp g) :=
  hom_ext rfl rfl

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