Uniform space structure on matrices

@[instance_reducible]

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

Equations

• Matrix.instUniformSpace m n 𝕜 = { toTopologicalSpace := instTopologicalSpaceMatrix, uniformity := Matrix.instUniformSpace._aux_1 m n 𝕜, symm := ⋯, comp := ⋯, nhds_eq_comap_uniformity := ⋯ }

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

theorem Matrix.uniformity (m : Type u_1) (n : Type u_2) (𝕜 : Type u_3) [UniformSpace 𝕜] : _root_.uniformity (Matrix m n 𝕜) = ⨅ (i : m), ⨅ (j : n), Filter.comap (fun (a : Matrix m n 𝕜 × Matrix m n 𝕜) => (a.1 i j, a.2 i j)) (_root_.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.instCompleteSpace (m : Type u_1) (n : Type u_2) (𝕜 : Type u_3) [UniformSpace 𝕜] [CompleteSpace 𝕜] : CompleteSpace (Matrix m n 𝕜)