map_map — Mathlib

English

Given subsemiring s of R and maps f: R → S, g: S → T, the successive image equals the image under the composition: (s.map f).map g = s.map (g ∘ f).

Русский

Пусть s ⊆ R — подполусемиринг и отображения f: R → S, g: S → T. Тогда последовательное отображение образа эквивалентно образу композиции: (s.map f).map g = s.map (g ∘ f).

LaTeX

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

Lean4

theorem map_map (g : G) (f : F) :
    (s.map (f : R →ₙ+* S)).map (g : S →ₙ+* T) = s.map ((g : S →ₙ+* T).comp (f : R →ₙ+* S)) :=
  SetLike.coe_injective <| Set.image_image _ _ _

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