Uniform space structure on matrices #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[protected, instance]
def
matrix.uniform_space
(m : Type u_1)
(n : Type u_2)
(π : Type u_3)
[uniform_space π] :
uniform_space (matrix m n π)
Equations
- matrix.uniform_space m n π = Pi.uniform_space (Ξ» (αΎ° : m), n β π)
theorem
matrix.uniformity
(m : Type u_1)
(n : Type u_2)
(π : Type u_3)
[uniform_space π] :
uniformity (matrix m n π) = β¨
(i : m) (j : n), filter.comap (Ξ» (a : matrix m n π Γ matrix m n π), (a.fst i j, a.snd i j)) (uniformity π)
theorem
matrix.uniform_continuous
(m : Type u_1)
(n : Type u_2)
(π : Type u_3)
[uniform_space π]
{Ξ² : Type u_4}
[uniform_space Ξ²]
{f : Ξ² β matrix m n π} :
uniform_continuous f β β (i : m) (j : n), uniform_continuous (Ξ» (x : Ξ²), f x i j)
@[protected, instance]
def
matrix.complete_space
(m : Type u_1)
(n : Type u_2)
(π : Type u_3)
[uniform_space π]
[complete_space π] :
complete_space (matrix m n π)
@[protected, instance]
def
matrix.separated_space
(m : Type u_1)
(n : Type u_2)
(π : Type u_3)
[uniform_space π]
[separated_space π] :
separated_space (matrix m n π)