# mathlibdocumentation

topology.uniform_space.matrix

# Uniform space structure on matrices #

@[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
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 : n π Γ 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 : Ξ² β n π} :
β β (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 π)