theorem Basis.toMatrix_continuous {ι : Type u_1} {R : Type u_2} {M : Type u_3} [AddCommGroup M] [Fintype ι] [TopologicalSpace M] [NontriviallyNormedField R] [Module R M] [IsTopologicalAddGroup M] [ContinuousSMul R M] [CompleteSpace R] [T2Space M] [FiniteDimensional R M] (B : Basis ι R M) : Continuous fun (v : ι → M) => B.toMatrix v