[GOAL]
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝ : UniformSpace 𝕜
⊢ UniformSpace (m → n → 𝕜)
[PROOFSTEP]
infer_instance
[GOAL]
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)) (𝓤 𝕜)
[PROOFSTEP]
erw [Pi.uniformity, Pi.uniformity]
[GOAL]
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)) (𝓤 𝕜)
[PROOFSTEP]
simp_rw [Filter.comap_iInf, Filter.comap_comap]
[GOAL]
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)) (𝓤 𝕜)
[PROOFSTEP]
rfl
[GOAL]
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝¹ : UniformSpace 𝕜
β : Type u_4
inst✝ : UniformSpace β
f : β → Matrix m n 𝕜
⊢ UniformContinuous f ↔ ∀ (i : m) (j : n), UniformContinuous fun x => f x i j
[PROOFSTEP]
simp only [UniformContinuous, Matrix.uniformity, Filter.tendsto_iInf, Filter.tendsto_comap_iff]
[GOAL]
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝¹ : UniformSpace 𝕜
β : Type u_4
inst✝ : UniformSpace β
f : β → Matrix m n 𝕜
⊢ (∀ (i : m) (i_1 : n),
      Filter.Tendsto ((fun a => (Prod.fst a i i_1, Prod.snd a i i_1)) ∘ fun x => (f x.fst, f x.snd)) (𝓤 β) (𝓤 𝕜)) ↔
    ∀ (i : m) (j : n), Filter.Tendsto (fun x => (f x.fst i j, f x.snd i j)) (𝓤 β) (𝓤 𝕜)
[PROOFSTEP]
apply Iff.intro
[GOAL]
case mp
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝¹ : UniformSpace 𝕜
β : Type u_4
inst✝ : UniformSpace β
f : β → Matrix m n 𝕜
⊢ (∀ (i : m) (i_1 : n),
      Filter.Tendsto ((fun a => (Prod.fst a i i_1, Prod.snd a i i_1)) ∘ fun x => (f x.fst, f x.snd)) (𝓤 β) (𝓤 𝕜)) →
    ∀ (i : m) (j : n), Filter.Tendsto (fun x => (f x.fst i j, f x.snd i j)) (𝓤 β) (𝓤 𝕜)
[PROOFSTEP]
intro a
[GOAL]
case mpr
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝¹ : UniformSpace 𝕜
β : Type u_4
inst✝ : UniformSpace β
f : β → Matrix m n 𝕜
⊢ (∀ (i : m) (j : n), Filter.Tendsto (fun x => (f x.fst i j, f x.snd i j)) (𝓤 β) (𝓤 𝕜)) →
    ∀ (i : m) (i_1 : n),
      Filter.Tendsto ((fun a => (Prod.fst a i i_1, Prod.snd a i i_1)) ∘ fun x => (f x.fst, f x.snd)) (𝓤 β) (𝓤 𝕜)
[PROOFSTEP]
intro a
[GOAL]
case mp
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝¹ : UniformSpace 𝕜
β : Type u_4
inst✝ : UniformSpace β
f : β → Matrix m n 𝕜
a :
  ∀ (i : m) (i_1 : n),
    Filter.Tendsto ((fun a => (Prod.fst a i i_1, Prod.snd a i i_1)) ∘ fun x => (f x.fst, f x.snd)) (𝓤 β) (𝓤 𝕜)
⊢ ∀ (i : m) (j : n), Filter.Tendsto (fun x => (f x.fst i j, f x.snd i j)) (𝓤 β) (𝓤 𝕜)
[PROOFSTEP]
apply a
[GOAL]
case mpr
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝¹ : UniformSpace 𝕜
β : Type u_4
inst✝ : UniformSpace β
f : β → Matrix m n 𝕜
a : ∀ (i : m) (j : n), Filter.Tendsto (fun x => (f x.fst i j, f x.snd i j)) (𝓤 β) (𝓤 𝕜)
⊢ ∀ (i : m) (i_1 : n),
    Filter.Tendsto ((fun a => (Prod.fst a i i_1, Prod.snd a i i_1)) ∘ fun x => (f x.fst, f x.snd)) (𝓤 β) (𝓤 𝕜)
[PROOFSTEP]
apply a
[GOAL]
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝¹ : UniformSpace 𝕜
inst✝ : CompleteSpace 𝕜
⊢ CompleteSpace (m → n → 𝕜)
[PROOFSTEP]
infer_instance
[GOAL]
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝¹ : UniformSpace 𝕜
inst✝ : SeparatedSpace 𝕜
⊢ SeparatedSpace (m → n → 𝕜)
[PROOFSTEP]
infer_instance
