isResiduallyFiniteImageOf

Indicates that one structure is the image of another under a homomorphism such that, for every nontrivial element in the source, some finite quotient of the image distinguishes its image from the identity (i.e., the image is residually finite relative to the source).