ι : Type u_3
l : Filter ι
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
hf' : UniformCauchySeqOnFilter f' l (𝓝 x)
hfg : Cauchy (map (fun n => f n x) l)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
⊢ UniformCauchySeqOnFilter f l (𝓝 x)
ι : Type u_3
l : Filter ι
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
hf' : UniformCauchySeqOnFilter f' l (𝓝 x)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasDerivAt (f n.fst) (f' n.fst n.snd) n.snd
hfg : Cauchy (map (fun n => f n x) l)
⊢ UniformCauchySeqOnFilter f l (𝓝 x)
simp_rw [hasDerivAt_iff_hasFDerivAt] at hf
no goals
ι : Type u_3
l : Filter ι
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
hf' : UniformCauchySeqOnFilter f' l (𝓝 x)
hfg : Cauchy (map (fun n => f n x) l)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
⊢ UniformCauchySeqOnFilter f l (𝓝 x)
exact uniformCauchySeqOnFilter_of_fderiv hf'.one_smulRight hf hfg