Uniform space structure on matrices #
instance
Matrix.instUniformSpace
(m : Type u_1)
(n : Type u_2)
(𝕜 : Type u_3)
[UniformSpace 𝕜]
:
UniformSpace (Matrix m n 𝕜)
Equations
- Matrix.instUniformSpace m n 𝕜 = inferInstance
instance
Matrix.instUniformAddGroup
(m : Type u_1)
(n : Type u_2)
(𝕜 : Type u_3)
[UniformSpace 𝕜]
[AddGroup 𝕜]
[UniformAddGroup 𝕜]
:
UniformAddGroup (Matrix m n 𝕜)
Equations
- ⋯ = ⋯
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 : Matrix m n 𝕜 × Matrix m n 𝕜) => (a.1 i j, a.2 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.instCompleteSpace
(m : Type u_1)
(n : Type u_2)
(𝕜 : Type u_3)
[UniformSpace 𝕜]
[CompleteSpace 𝕜]
:
CompleteSpace (Matrix m n 𝕜)
Equations
- ⋯ = ⋯
instance
Matrix.instT0Space
(m : Type u_1)
(n : Type u_2)
(𝕜 : Type u_3)
[UniformSpace 𝕜]
[T0Space 𝕜]
:
Equations
- ⋯ = ⋯