∀ {𝕜 : Type u_1} [hnorm : NontriviallyNormedField 𝕜] {E : Type u_3} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [CompleteSpace 𝕜] {ι : Type u_2}
  [inst_6 : Finite ι] (v : Module.Basis ι 𝕜 E), Continuous v.equivFun.invFun