ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
s : Set 𝕜
hs : IsOpen s
hf' : TendstoLocallyUniformlyOn (deriv ∘ f) g' l s
hf : ∀ᶠ (n : ι) in l, DifferentiableOn 𝕜 (f n) s
hfg : ∀ (x : 𝕜), x ∈ s → Tendsto (fun n => f n x) l (𝓝 (g x))
hx : x ∈ s
⊢ ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), x ∈ s → HasDerivAt (fun x => f n x) ((deriv ∘ f) n x) x
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
s : Set 𝕜
hs : IsOpen s
hf' : TendstoLocallyUniformlyOn (deriv ∘ f) g' l s
hf : ∀ᶠ (n : ι) in l, DifferentiableOn 𝕜 (f n) s
hfg : ∀ (x : 𝕜), x ∈ s → Tendsto (fun n => f n x) l (𝓝 (g x))
hx : x ∈ s
⊢ HasDerivAt g (g' x) x
refine' hasDerivAt_of_tendstoLocallyUniformlyOn hs hf' _ hfg hx
no goals
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
s : Set 𝕜
hs : IsOpen s
hf' : TendstoLocallyUniformlyOn (deriv ∘ f) g' l s
hf : ∀ᶠ (n : ι) in l, DifferentiableOn 𝕜 (f n) s
hfg : ∀ (x : 𝕜), x ∈ s → Tendsto (fun n => f n x) l (𝓝 (g x))
hx : x ∈ s
⊢ ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), x ∈ s → HasDerivAt (fun x => f n x) ((deriv ∘ f) n x) x
filter_upwards [hf]with n h z hz using((h z hz).differentiableAt (hs.mem_nhds hz)).hasDerivAt