ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedSpace 𝕜 E
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst✝ : NeBot l
s : Set E
hs : IsOpen s
hf' : TendstoLocallyUniformlyOn (fderiv 𝕜 ∘ f) g' l s
hf : ∀ (n : ι), DifferentiableOn 𝕜 (f n) s
hfg : ∀ (x : E), x ∈ s → Tendsto (fun n => f n x) l (𝓝 (g x))
hx : x ∈ s
n : ι
z : E
hz : z ∈ s
⊢ HasFDerivAt (fun x => f n x) ((fderiv 𝕜 ∘ f) n z) z
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedSpace 𝕜 E
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst✝ : NeBot l
s : Set E
hs : IsOpen s
hf' : TendstoLocallyUniformlyOn (fderiv 𝕜 ∘ f) g' l s
hf : ∀ (n : ι), DifferentiableOn 𝕜 (f n) s
hfg : ∀ (x : E), x ∈ s → Tendsto (fun n => f n x) l (𝓝 (g x))
hx : x ∈ s
⊢ HasFDerivAt g (g' x) x
refine' hasFDerivAt_of_tendstoLocallyUniformlyOn hs hf' (fun n z hz => _) hfg hx
no goals
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedSpace 𝕜 E
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst✝ : NeBot l
s : Set E
hs : IsOpen s
hf' : TendstoLocallyUniformlyOn (fderiv 𝕜 ∘ f) g' l s
hf : ∀ (n : ι), DifferentiableOn 𝕜 (f n) s
hfg : ∀ (x : E), x ∈ s → Tendsto (fun n => f n x) l (𝓝 (g x))
hx : x ∈ s
n : ι
z : E
hz : z ∈ s
⊢ HasFDerivAt (fun x => f n x) ((fderiv 𝕜 ∘ f) n z) z
exact ((hf n z hz).differentiableAt (hs.mem_nhds hz)).hasFDerivAt