map_map_apply — Mathlib

English

For f: G →* H and g: H →* I, and x ∈ Abelianization G, map g (map f x) = map (g ∘ f) x.

Русский

Для f: G →* H, g: H →* I и x ∈ Abelianization(G), выполняется map g (map f x) = map (g ∘ f) x.

LaTeX

$$$$ \\mathrm{map}\, g \\big( \\mathrm{map}\, f (x) \\big) = \\mathrm{map}\\big( g \\circ f \\big) (x). $$$$

Lean4

@[simp]
theorem map_map_apply {I : Type w} [Group I] {g : H →* I} {x : Abelianization G} : map g (map f x) = map (g.comp f) x :=
  DFunLike.congr_fun (map_comp _ _) x

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