theorem Subalgebra.map_centralizer_le_centralizer_image {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (s : Set A) (f : A →ₐ[R] B) : map f (centralizer R s) ≤ centralizer R (⇑f '' s)