α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace γ
h : TendstoLocallyUniformlyOn F f p univ
g : γ → α
cg : Continuous g
⊢ TendstoLocallyUniformlyOn (fun n => F n ∘ g) (f ∘ g) p univ
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace γ
h : TendstoLocallyUniformly F f p
g : γ → α
cg : Continuous g
⊢ TendstoLocallyUniformly (fun n => F n ∘ g) (f ∘ g) p
rw [← tendstoLocallyUniformlyOn_univ] at h⊢
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace γ
h : TendstoLocallyUniformlyOn F f p univ
g : γ → α
cg : ContinuousOn g univ
⊢ TendstoLocallyUniformlyOn (fun n => F n ∘ g) (f ∘ g) p univ
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace γ
h : TendstoLocallyUniformlyOn F f p univ
g : γ → α
cg : Continuous g
⊢ TendstoLocallyUniformlyOn (fun n => F n ∘ g) (f ∘ g) p univ
rw [continuous_iff_continuousOn_univ] at cg
no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace γ
h : TendstoLocallyUniformlyOn F f p univ
g : γ → α
cg : ContinuousOn g univ
⊢ TendstoLocallyUniformlyOn (fun n => F n ∘ g) (f ∘ g) p univ
exact h.comp _ (mapsTo_univ _ _) cg