𝕜 : Type u_2
E : Type u_1
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g✝ : E → F
p pf pg : FormalMultilinearSeries 𝕜 E F
x✝ : E
r r' : ℝ≥0∞
s : Set E
g : F →L[𝕜] G
h : AnalyticOn 𝕜 f s
x : E
hx : x ∈ s
⊢ AnalyticAt 𝕜 (↑g ∘ f) x
𝕜 : Type u_2
E : Type u_1
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g✝ : E → F
p pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r r' : ℝ≥0∞
s : Set E
g : F →L[𝕜] G
h : AnalyticOn 𝕜 f s
⊢ AnalyticOn 𝕜 (↑g ∘ f) s
rintro x hx
case intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g✝ : E → F
p✝ pf pg : FormalMultilinearSeries 𝕜 E F
x✝ : E
r✝ r' : ℝ≥0∞
s : Set E
g : F →L[𝕜] G
h : AnalyticOn 𝕜 f s
x : E
hx : x ∈ s
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
⊢ AnalyticAt 𝕜 (↑g ∘ f) x
𝕜 : Type u_2
E : Type u_1
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g✝ : E → F
p pf pg : FormalMultilinearSeries 𝕜 E F
x✝ : E
r r' : ℝ≥0∞
s : Set E
g : F →L[𝕜] G
h : AnalyticOn 𝕜 f s
x : E
hx : x ∈ s
⊢ AnalyticAt 𝕜 (↑g ∘ f) x
rcases h x hx with ⟨p, r, hp⟩
no goals
case intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g✝ : E → F
p✝ pf pg : FormalMultilinearSeries 𝕜 E F
x✝ : E
r✝ r' : ℝ≥0∞
s : Set E
g : F →L[𝕜] G
h : AnalyticOn 𝕜 f s
x : E
hx : x ∈ s
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
⊢ AnalyticAt 𝕜 (↑g ∘ f) x
exact ⟨g.compFormalMultilinearSeries p, r, g.comp_hasFPowerSeriesOnBall hp⟩