map_map — Mathlib

English

The composition of two submonoid maps equals the single map of the composed homomorphism: (S.map f).map g = S.map (g ∘ f).

Русский

Сечение двух отображений подмономодов равняется отображению композиции гомоморфизмов: (S.map f).map g = S.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 _ _
      _
        -- The simpNF linter says that the LHS can be simplified via `Submonoid.mem_map`.
        -- However this is a higher priority lemma.
        -- It seems the side condition `hf` is not applied by `simpNF`.
        -- https://github.com/leanprover/std4/issues/207

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