m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝ : UniformSpace 𝕜
⊢ (⨅ (i : m),
      Filter.comap (fun a => (Prod.fst a i, Prod.snd a i))
        (⨅ (i : n), Filter.comap (fun a => (Prod.fst a i, Prod.snd a i)) (𝓤 𝕜))) =
    ⨅ (i : m) (j : n), Filter.comap (fun a => (Prod.fst a i j, Prod.snd a i j)) (𝓤 𝕜)
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝ : UniformSpace 𝕜
⊢ 𝓤 (Matrix m n 𝕜) = ⨅ (i : m) (j : n), Filter.comap (fun a => (Prod.fst a i j, Prod.snd a i j)) (𝓤 𝕜)
erw [Pi.uniformity, Pi.uniformity]
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝ : UniformSpace 𝕜
⊢ (⨅ (i : m) (i_1 : n),
      Filter.comap ((fun a => (Prod.fst a i_1, Prod.snd a i_1)) ∘ fun a => (Prod.fst a i, Prod.snd a i)) (𝓤 𝕜)) =
    ⨅ (i : m) (j : n), Filter.comap (fun a => (Prod.fst a i j, Prod.snd a i j)) (𝓤 𝕜)
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝ : UniformSpace 𝕜
⊢ (⨅ (i : m),
      Filter.comap (fun a => (Prod.fst a i, Prod.snd a i))
        (⨅ (i : n), Filter.comap (fun a => (Prod.fst a i, Prod.snd a i)) (𝓤 𝕜))) =
    ⨅ (i : m) (j : n), Filter.comap (fun a => (Prod.fst a i j, Prod.snd a i j)) (𝓤 𝕜)
simp_rw [Filter.comap_iInf, Filter.comap_comap]
no goals
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝ : UniformSpace 𝕜
⊢ (⨅ (i : m) (i_1 : n),
      Filter.comap ((fun a => (Prod.fst a i_1, Prod.snd a i_1)) ∘ fun a => (Prod.fst a i, Prod.snd a i)) (𝓤 𝕜)) =
    ⨅ (i : m) (j : n), Filter.comap (fun a => (Prod.fst a i j, Prod.snd a i j)) (𝓤 𝕜)
rfl