map_map — Mathlib

English

For any f', g', f, g and x in M ∗ N, map f' g' (map f g x) = map (f' ∘ f) (g' ∘ g) x.

Русский

Для любых f', g', f, g и x ∈ M ∗ N выполняется equality: map f' g' (map f g x) = map (f' ∘ f) (g' ∘ g) x.

LaTeX

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

Lean4

@[to_additive]
theorem map_map {M'' N''} [MulOneClass M''] [MulOneClass N''] (f' : M' →* M'') (g' : N' →* N'') (f : M →* M')
    (g : N →* N') (x : M ∗ N) : map f' g' (map f g x) = map (f'.comp f) (g'.comp g) x :=
  DFunLike.congr_fun (map_comp_map f' g' f g) x

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