α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
h : ContinuousWithinAt f univ x
hg : Tendsto g p (𝓝 x)
hunif : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
⊢ Tendsto (fun n => F n (g n)) p (𝓝 (f x))
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
h : ContinuousAt f x
hg : Tendsto g p (𝓝 x)
hunif : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
⊢ Tendsto (fun n => F n (g n)) p (𝓝 (f x))
rw [← continuousWithinAt_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 α
h : ContinuousWithinAt f univ x
hg : Tendsto g p (𝓝[univ] x)
hunif : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝[univ] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
⊢ Tendsto (fun n => F n (g n)) p (𝓝 (f x))
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
h : ContinuousWithinAt f univ x
hg : Tendsto g p (𝓝 x)
hunif : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
⊢ Tendsto (fun n => F n (g n)) p (𝓝 (f x))
rw [← nhdsWithin_univ] at hunif hg
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 α
h : ContinuousWithinAt f univ x
hg : Tendsto g p (𝓝[univ] x)
hunif : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝[univ] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
⊢ Tendsto (fun n => F n (g n)) p (𝓝 (f x))
exact tendsto_comp_of_locally_uniform_limit_within h hg hunif