Uniform space structure on matrices

instance Matrix.instUniformSpaceMatrix (m : Type u_1) (n : Type u_2) (𝕜 : Type u_3) [UniformSpace 𝕜] : UniformSpace (Matrix m n 𝕜)

theorem Matrix.uniformity (m : Type u_1) (n : Type u_2) (𝕜 : Type u_3) [UniformSpace 𝕜] : uniformity (Matrix m n 𝕜) = ⨅ (i : m) (j : n), Filter.comap (fun a => (Prod.fst (Matrix m n 𝕜) (Matrix m n 𝕜) a i j, Prod.snd (Matrix m n 𝕜) (Matrix m n 𝕜) a i j)) (uniformity 𝕜)

theorem Matrix.uniformContinuous (m : Type u_1) (n : Type u_2) (𝕜 : Type u_3) [UniformSpace 𝕜] {β : Type u_4} [UniformSpace β] {f : β → Matrix m n 𝕜} : UniformContinuous f ↔ ∀ (i : m) (j : n), UniformContinuous fun x => f x i j

instance Matrix.instCompleteSpaceMatrixInstUniformSpaceMatrix (m : Type u_1) (n : Type u_2) (𝕜 : Type u_3) [UniformSpace 𝕜] [CompleteSpace 𝕜] : CompleteSpace (Matrix m n 𝕜)

instance Matrix.instSeparatedSpaceMatrixInstUniformSpaceMatrix (m : Type u_1) (n : Type u_2) (𝕜 : Type u_3) [UniformSpace 𝕜] [SeparatedSpace 𝕜] : SeparatedSpace (Matrix m n 𝕜)