∀ {k : Type u_4} {P₁ : Type u_1} {P₂ : Type u_3} {P₃ : Type u_2} {V₁ : Type u_7} {V₂ : Type u_5} {V₃ : Type u_6}
  [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁]
  [inst_4 : TopologicalSpace P₁] [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂]
  [inst_8 : TopologicalSpace P₂] [inst_9 : AddCommGroup V₃] [inst_10 : Module k V₃] [inst_11 : AddTorsor V₃ P₃]
  [inst_12 : TopologicalSpace P₃] (e : P₁ ≃ᴬ[k] P₂) (e' : P₂ ≃ᴬ[k] P₃), Continuous ((↑e').toFun ∘ ⇑(↑e).toEquiv)