internlm/Lean-Github huggingface dataset:
Theorem: differentiable_iff_analytic2
Proof state before:
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
⊢ DifferentiableOn ℂ f s ↔ AnalyticOn ℂ f s
Tactic:
constructor
Proof state after:
case mp
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
⊢ DifferentiableOn ℂ f s → AnalyticOn ℂ f s

case mpr
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
⊢ AnalyticOn ℂ f s → DifferentiableOn ℂ f s
Theorem: differentiable_iff_analytic2
Proof state before:
case mp
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
⊢ DifferentiableOn ℂ f s → AnalyticOn ℂ f s
Tactic:
intro d
Proof state after:
case mp
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
⊢ AnalyticOn ℂ f s
Theorem: differentiable_iff_analytic2
Proof state before:
case mp
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
⊢ AnalyticOn ℂ f s
Tactic:
apply osgood o d.continuousOn
Proof state after:
case mp.fa0
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
⊢ ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0

case mp.fa1
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
⊢ ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
Theorem: differentiable_iff_analytic2
Proof state before:
case mp.fa0
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
⊢ ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
Tactic:
intro z0 z1 zs
Proof state after:
case mp.fa0
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
⊢ AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
Theorem: differentiable_iff_analytic2
Proof state before:
case mp.fa0
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
⊢ AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
Tactic:
rcases Metric.isOpen_iff.mp o (z0, z1) zs with ⟨r, rp, rs⟩
Proof state after:
case mp.fa0.intro.intro
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
Theorem: differentiable_iff_analytic2
Proof state before:
case mp.fa0.intro.intro
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
Tactic:
have d0 : DifferentiableOn ℂ (fun z0 ↦ f (z0, z1)) (ball z0 r) := by
  apply DifferentiableOn.comp d
  exact DifferentiableOn.prod differentiableOn_id (differentiableOn_const _)
  intro z0 z0s; apply rs; simp at z0s ⊢; assumption
Proof state after:
case mp.fa0.intro.intro
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
d0 : DifferentiableOn ℂ (fun z0 => f (z0, z1)) (ball z0 r)
⊢ AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
Theorem: differentiable_iff_analytic2
Proof state before:
case mp.fa0.intro.intro
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
d0 : DifferentiableOn ℂ (fun z0 => f (z0, z1)) (ball z0 r)
⊢ AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
Tactic:
exact (analyticOn_iff_differentiableOn isOpen_ball).mpr d0 z0 (Metric.mem_ball_self rp)
Proof state after:
no goals
Theorem: differentiable_iff_analytic2
Proof state before:
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ DifferentiableOn ℂ (fun z0 => f (z0, z1)) (ball z0 r)
Tactic:
apply DifferentiableOn.comp d
Proof state after:
case hf
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ DifferentiableOn ℂ (fun z0 => (z0, z1)) (ball z0 r)

case st
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ Set.MapsTo (fun z0 => (z0, z1)) (ball z0 r) s
Theorem: differentiable_iff_analytic2
Proof state before:
case hf
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ DifferentiableOn ℂ (fun z0 => (z0, z1)) (ball z0 r)

case st
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ Set.MapsTo (fun z0 => (z0, z1)) (ball z0 r) s
Tactic:
exact DifferentiableOn.prod differentiableOn_id (differentiableOn_const _)
Proof state after:
case st
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ Set.MapsTo (fun z0 => (z0, z1)) (ball z0 r) s
Theorem: differentiable_iff_analytic2
Proof state before:
case st
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ Set.MapsTo (fun z0 => (z0, z1)) (ball z0 r) s
Tactic:
intro z0 z0s
Proof state after:
case st
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0✝ z1 : ℂ
zs : (z0✝, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0✝, z1) r ⊆ s
z0 : ℂ
z0s : z0 ∈ ball z0✝ r
⊢ (fun z0 => (z0, z1)) z0 ∈ s
Theorem: differentiable_iff_analytic2
Proof state before:
case st
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0✝ z1 : ℂ
zs : (z0✝, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0✝, z1) r ⊆ s
z0 : ℂ
z0s : z0 ∈ ball z0✝ r
⊢ (fun z0 => (z0, z1)) z0 ∈ s
Tactic:
apply rs
Proof state after:
case st.a
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0✝ z1 : ℂ
zs : (z0✝, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0✝, z1) r ⊆ s
z0 : ℂ
z0s : z0 ∈ ball z0✝ r
⊢ (fun z0 => (z0, z1)) z0 ∈ ball (z0✝, z1) r
Theorem: differentiable_iff_analytic2
Proof state before:
case st.a
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0✝ z1 : ℂ
zs : (z0✝, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0✝, z1) r ⊆ s
z0 : ℂ
z0s : z0 ∈ ball z0✝ r
⊢ (fun z0 => (z0, z1)) z0 ∈ ball (z0✝, z1) r
Tactic:
simp at z0s ⊢
Proof state after:
case st.a
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0✝ z1 : ℂ
zs : (z0✝, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0✝, z1) r ⊆ s
z0 : ℂ
z0s : dist z0 z0✝ < r
⊢ dist z0 z0✝ < r
Theorem: differentiable_iff_analytic2
Proof state before:
case st.a
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0✝ z1 : ℂ
zs : (z0✝, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0✝, z1) r ⊆ s
z0 : ℂ
z0s : dist z0 z0✝ < r
⊢ dist z0 z0✝ < r
Tactic:
assumption
Proof state after:
no goals
Theorem: differentiable_iff_analytic2
Proof state before:
case mp.fa1
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
⊢ ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
Tactic:
intro z0 z1 zs
Proof state after:
case mp.fa1
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
⊢ AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
Theorem: differentiable_iff_analytic2
Proof state before:
case mp.fa1
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
⊢ AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
Tactic:
rcases Metric.isOpen_iff.mp o (z0, z1) zs with ⟨r, rp, rs⟩
Proof state after:
case mp.fa1.intro.intro
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
Theorem: differentiable_iff_analytic2
Proof state before:
case mp.fa1.intro.intro
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
Tactic:
have d1 : DifferentiableOn ℂ (fun z1 ↦ f (z0, z1)) (ball z1 r) := by
  apply DifferentiableOn.comp d
  exact DifferentiableOn.prod (differentiableOn_const _) differentiableOn_id
  intro z1 z1s; apply rs; simp at z1s ⊢; assumption
Proof state after:
case mp.fa1.intro.intro
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
d1 : DifferentiableOn ℂ (fun z1 => f (z0, z1)) (ball z1 r)
⊢ AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
Theorem: differentiable_iff_analytic2
Proof state before:
case mp.fa1.intro.intro
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
d1 : DifferentiableOn ℂ (fun z1 => f (z0, z1)) (ball z1 r)
⊢ AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
Tactic:
exact (analyticOn_iff_differentiableOn isOpen_ball).mpr d1 z1 (Metric.mem_ball_self rp)
Proof state after:
no goals
Theorem: differentiable_iff_analytic2
Proof state before:
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ DifferentiableOn ℂ (fun z1 => f (z0, z1)) (ball z1 r)
Tactic:
apply DifferentiableOn.comp d
Proof state after:
case hf
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ DifferentiableOn ℂ (fun z1 => (z0, z1)) (ball z1 r)

case st
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ Set.MapsTo (fun z1 => (z0, z1)) (ball z1 r) s
Theorem: differentiable_iff_analytic2
Proof state before:
case hf
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ DifferentiableOn ℂ (fun z1 => (z0, z1)) (ball z1 r)

case st
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ Set.MapsTo (fun z1 => (z0, z1)) (ball z1 r) s
Tactic:
exact DifferentiableOn.prod (differentiableOn_const _) differentiableOn_id
Proof state after:
case st
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ Set.MapsTo (fun z1 => (z0, z1)) (ball z1 r) s
Theorem: differentiable_iff_analytic2
Proof state before:
case st
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ Set.MapsTo (fun z1 => (z0, z1)) (ball z1 r) s
Tactic:
intro z1 z1s
Proof state after:
case st
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1✝ : ℂ
zs : (z0, z1✝) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1✝) r ⊆ s
z1 : ℂ
z1s : z1 ∈ ball z1✝ r
⊢ (fun z1 => (z0, z1)) z1 ∈ s
Theorem: differentiable_iff_analytic2
Proof state before:
case st
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1✝ : ℂ
zs : (z0, z1✝) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1✝) r ⊆ s
z1 : ℂ
z1s : z1 ∈ ball z1✝ r
⊢ (fun z1 => (z0, z1)) z1 ∈ s
Tactic:
apply rs
Proof state after:
case st.a
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1✝ : ℂ
zs : (z0, z1✝) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1✝) r ⊆ s
z1 : ℂ
z1s : z1 ∈ ball z1✝ r
⊢ (fun z1 => (z0, z1)) z1 ∈ ball (z0, z1✝) r