Theorem: analyticOn_univ_iff_differentiable (Ray/Analytic/HolomorphicUpstream.lean)

State before:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → E
⊢ AnalyticOn ℂ f univ ↔ Differentiable ℂ f
Tactic:
simp only [←  differentiableOn_univ]
State after:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → E
⊢ AnalyticOn ℂ f univ ↔ DifferentiableOn ℂ f univ

State before:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → E
⊢ AnalyticOn ℂ f univ ↔ DifferentiableOn ℂ f univ
Tactic:
exact analyticOn_iff_differentiableOn isOpen_univ
State after:
no goals