map_map — Mathlib

English

Applying two maps in sequence is the same as applying their composition: map g (map f S) = map (g ∘ f) S.

Русский

Применение двух отображений последовательно даёт тот же результат, что и применение их композиции: map g (map f S) = map (g ∘ f) S.

LaTeX

$$map(g, map(f,S)) = map(g ∘ f, S).$$

Lean4

theorem map_map (S : NonUnitalStarSubalgebra R A) (g : B →⋆ₙₐ[R] C) (f : A →⋆ₙₐ[R] B) :
    (S.map f).map g = S.map (g.comp f) :=
  SetLike.coe_injective <| Set.image_image _ _ _

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