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 _ _ _