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 𝕜)