∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {B : Set X} {H : Type u_3} {Y : Type u_4}
  [inst_2 : VAdd H Y] {φ : G → H} (j : X →ₑ[φ] Y),
  Function.Surjective φ → Function.Injective ⇑j → AddAction.IsBlock G B → AddAction.IsBlock H (⇑j '' B)