∀ {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  {module_M : Module R M} (p q : Submodule R M) (h : p = q), Continuous (↑(LinearEquiv.ofEq p q h)).toFun