map_map — Mathlib

English

Let S be a StarSubalgebra of A. For star-algebra homomorphisms f: A →⋆ₐ[R] B and g: B →⋆ₐ[R] C, the two-step image of S equals the image of S under the composition g ∘ f: (S.map f).map g = S.map (g.comp f).

Русский

Пусть S — звездная подсалгебра A. Для звездно-алгебрических гомоморфизмов f: A →⋆ₐ[R] B и g: B →⋆ₐ[R] C справедливо, что двукратное отображение S равно отображению через композицию: (S.map f).map g = S.map (g.comp f).

LaTeX

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

Lean4

theorem map_map (S : StarSubalgebra 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 _ _ _

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