no goals
𝓕 : Type ?u.502213
𝕜 : Type ?u.502216
α : Type ?u.502219
ι : Type u_2
κ : Type u_1
E : Type ?u.502228
F : Type ?u.502231
G : Type u_3
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s✝ : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : ι → κ → G
s : Set κ
l : Filter ι
⊢ TendstoUniformlyOn f 1 l s ↔ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (i : ι) in l, ∀ (x : κ), x ∈ s → ‖f i x‖ < ε
simp_rw [tendstoUniformlyOn_iff, Pi.one_apply, dist_one_left]