∀ {R : Type u_2} [inst : Ring R] [inst_1 : TopologicalSpace R] {M : ModuleCat R} {I : Type u_3} {X : I → TopModuleCat R}
  (f : (i : I) → (X i).toModuleCat ⟶ M), ContinuousAdd ↑(TopModuleCat.coinduced f).toModuleCat