α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
h : TendstoUniformlyOnFilter F f p ⊤
g : γ → α
⊢ TendstoUniformlyOnFilter (fun n => F n ∘ g) (f ∘ g) p ⊤
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
h : TendstoUniformly F f p
g : γ → α
⊢ TendstoUniformly (fun n => F n ∘ g) (f ∘ g) p
rw [tendstoUniformly_iff_tendstoUniformlyOnFilter] at h⊢
no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
h : TendstoUniformlyOnFilter F f p ⊤
g : γ → α
⊢ TendstoUniformlyOnFilter (fun n => F n ∘ g) (f ∘ g) p ⊤
simpa [principal_univ, comap_principal] using h.comp g