α : Type u_1
β : Type u_2
γ : Type ?u.45029
ι : Type u_3
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
F : ι → α →ᵤ β
f : α →ᵤ β
⊢ (∀ (i : Set (β × β)), i ∈ 𝓤 β → ∀ᶠ (x : ι) in p, F x ∈ {g | (f, g) ∈ UniformFun.gen α β i}) ↔
    ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ u
α : Type u_1
β : Type u_2
γ : Type ?u.45029
ι : Type u_3
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
F : ι → α →ᵤ β
f : α →ᵤ β
⊢ Tendsto F p (𝓝 f) ↔ TendstoUniformly F f p
rw [(UniformFun.hasBasis_nhds α β f).tendsto_right_iff, TendstoUniformly]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.45029
ι : Type u_3
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
F : ι → α →ᵤ β
f : α →ᵤ β
⊢ (∀ (i : Set (β × β)), i ∈ 𝓤 β → ∀ᶠ (x : ι) in p, F x ∈ {g | (f, g) ∈ UniformFun.gen α β i}) ↔
    ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ u
exact Iff.rfl