Documentation

Mathlib.Topology.UniformSpace.Matrix

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
instance Matrix.instUniformAddGroup (m : Type u_1) (n : Type u_2) (𝕜 : Type u_3) [UniformSpace 𝕜] [AddGroup 𝕜] [UniformAddGroup 𝕜] :
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 𝕜] :
Equations
  • =
instance Matrix.instT0Space (m : Type u_1) (n : Type u_2) (𝕜 : Type u_3) [UniformSpace 𝕜] [T0Space 𝕜] :
T0Space (Matrix m n 𝕜)
Equations
  • =