English
For a star-algebra homomorphism f, the image of the adjoin of s in A maps to the adjoin of the image of s in B.
Русский
Образ подалгебры adjoin_R s через f совпадает с подалгеброй, порождённой образами элементов s.
LaTeX
$$$ \\mathrm{map}\\; f\\; (\\mathrm{adjoin}_R s) = \\mathrm{adjoin}_R (f''s) $$$
Lean4
theorem map_adjoin (f : A →⋆ₐ[R] B) (s : Set A) : map f (adjoin R s) = adjoin R (f '' s) :=
GaloisConnection.l_comm_of_u_comm Set.image_preimage (gc_map_comap f) StarAlgebra.gc StarAlgebra.gc fun _ => rfl