m : Type u_2
n : Type u_3
𝕜 : Type u_4
inst✝¹ : UniformSpace 𝕜
β : Type u_1
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)) (𝓤 β) (𝓤 𝕜)
m : Type u_2
n : Type u_3
𝕜 : Type u_4
inst✝¹ : UniformSpace 𝕜
β : Type u_1
inst✝ : UniformSpace β
f : β → Matrix m n 𝕜
⊢ UniformContinuous f ↔ ∀ (i : m) (j : n), UniformContinuous fun x => f x i j
simp only [UniformContinuous, Matrix.uniformity, Filter.tendsto_iInf, Filter.tendsto_comap_iff]
no goals
m : Type u_2
n : Type u_3
𝕜 : Type u_4
inst✝¹ : UniformSpace 𝕜
β : Type u_1
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)) (𝓤 β) (𝓤 𝕜)
apply Iff.intro <;> intro a <;> apply a