∀ {M : Type u_6} {N : Type u_7} {F : Type u_8} [inst : Mul M] [inst_1 : Mul N] [inst_2 : FunLike F M N]
  [MulHomClass F M N] [inst_4 : TopologicalSpace M] [inst_5 : TopologicalSpace N] [ContinuousMul N] (f : F),
  Topology.IsInducing ⇑f → ContinuousMul M