internlm/Lean-Github huggingface dataset:
Theorem: nontrivial_local_of_global
Proof state before:
case nonconst
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
z : ℂ
e r : ℝ
fa : AnalyticOn ℂ f (closedBall z r)
rp : 0 < r
ep : 0 < e
fh : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (closedBall z r)
zs : z ∈ closedBall z r
ef : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
zrs : z + ↑r ∈ sphere z r
⊢ ∃ x, ∃ (_ : x ∈ sphere z r), ‖f x - f z‖ < e
Tactic:
use z + r, zrs
Proof state after:
case h
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
z : ℂ
e r : ℝ
fa : AnalyticOn ℂ f (closedBall z r)
rp : 0 < r
ep : 0 < e
fh : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (closedBall z r)
zs : z ∈ closedBall z r
ef : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
zrs : z + ↑r ∈ sphere z r
⊢ ‖f (z + ↑r) - f z‖ < e
Theorem: nontrivial_local_of_global
Proof state before:
case h
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
z : ℂ
e r : ℝ
fa : AnalyticOn ℂ f (closedBall z r)
rp : 0 < r
ep : 0 < e
fh : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (closedBall z r)
zs : z ∈ closedBall z r
ef : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
zrs : z + ↑r ∈ sphere z r
⊢ ‖f (z + ↑r) - f z‖ < e
Tactic:
simp only [fh.const_of_locally_const' zs (convex_closedBall z r).isPreconnected ef (z + r)
    (Metric.sphere_subset_closedBall zrs),
  sub_self, norm_zero, ep]
Proof state after:
no goals
Theorem: nontrivial_local_of_global
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
z : ℂ
e r : ℝ
fa : AnalyticOn ℂ f (closedBall z r)
rp : 0 < r
ep : 0 < e
fh : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (closedBall z r)
zs : z ∈ closedBall z r
ef : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
⊢ z + ↑r ∈ sphere z r
Tactic:
simp only [mem_sphere, Complex.dist_eq, add_sub_cancel_left, Complex.abs_ofReal, abs_of_pos rp]
Proof state after:
no goals
Theorem: AnalyticOn.ball_subset_image_closedBall_param
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
⊢ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r ∈ 𝓝 (c, f c z)
Tactic:
have fn : ∀ d, d ∈ u → ∃ᶠ w in 𝓝 z, f d w ≠ f d z := by
  refine fun d m ↦ (nontrivial_local_of_global (fa.along_snd.mono ?_) rp ep (ef d m)).nonconst
  simp only [← closedBall_prod_same, mem_prod_eq, setOf_mem_eq, iff_true_iff.mpr m,
    true_and_iff, subset_refl]
Proof state after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
⊢ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r ∈ 𝓝 (c, f c z)
Theorem: AnalyticOn.ball_subset_image_closedBall_param
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
⊢ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r ∈ 𝓝 (c, f c z)
Tactic:
have op : ∀ d, d ∈ u → ball (f d z) (e / 2) ⊆ f d '' closedBall z r := by
  intro d du; refine DiffContOnCl.ball_subset_image_closedBall ?_ rp (ef d du) (fn d du)
  have e : f d = uncurry f ∘ fun w ↦ (d, w) := rfl
  rw [e]; apply DifferentiableOn.diffContOnCl; apply AnalyticOn.differentiableOn
  refine fa.comp (analyticOn_const.prod (analyticOn_id _)) ?_
  intro w wr; simp only [closure_ball _ rp.ne'] at wr
  simp only [← closedBall_prod_same, mem_prod_eq, du, wr, true_and_iff, du]
Proof state after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
⊢ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r ∈ 𝓝 (c, f c z)
Theorem: AnalyticOn.ball_subset_image_closedBall_param
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
⊢ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r ∈ 𝓝 (c, f c z)
Tactic:
rcases Metric.continuousAt_iff.mp
    (fa (c, z) (mk_mem_prod (mem_of_mem_nhds un) (mem_closedBall_self rp.le))).continuousAt
    (e / 4) (by linarith) with
  ⟨s, sp, sh⟩
Proof state after:
case intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
⊢ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r ∈ 𝓝 (c, f c z)
Theorem: AnalyticOn.ball_subset_image_closedBall_param
Proof state before:
case intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
⊢ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r ∈ 𝓝 (c, f c z)
Tactic:
rw [mem_nhds_prod_iff]
Proof state after:
case intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
⊢ ∃ u_1 ∈ 𝓝 c, ∃ v ∈ 𝓝 (f c z), u_1 ×ˢ v ⊆ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r
Theorem: AnalyticOn.ball_subset_image_closedBall_param
Proof state before:
case intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
⊢ ∃ u_1 ∈ 𝓝 c, ∃ v ∈ 𝓝 (f c z), u_1 ×ˢ v ⊆ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r
Tactic:
refine ⟨u ∩ ball c s, Filter.inter_mem un (Metric.ball_mem_nhds c (by linarith)), ?_⟩
Proof state after:
case intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
⊢ ∃ v ∈ 𝓝 (f c z), (u ∩ ball c s) ×ˢ v ⊆ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r
Theorem: AnalyticOn.ball_subset_image_closedBall_param
Proof state before:
case intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
⊢ ∃ v ∈ 𝓝 (f c z), (u ∩ ball c s) ×ˢ v ⊆ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r
Tactic:
use ball (f c z) (e / 4), Metric.ball_mem_nhds _ (by linarith)
Proof state after:
case right
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
⊢ (u ∩ ball c s) ×ˢ ball (f c z) (e / 4) ⊆ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r
Theorem: AnalyticOn.ball_subset_image_closedBall_param
Proof state before:
case right
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
⊢ (u ∩ ball c s) ×ˢ ball (f c z) (e / 4) ⊆ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r
Tactic:
intro ⟨d, w⟩ m
Proof state after:
case right
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
d w : ℂ
m : (d, w) ∈ (u ∩ ball c s) ×ˢ ball (f c z) (e / 4)
⊢ (d, w) ∈ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r
Theorem: AnalyticOn.ball_subset_image_closedBall_param
Proof state before:
case right
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
d w : ℂ
m : (d, w) ∈ (u ∩ ball c s) ×ˢ ball (f c z) (e / 4)
⊢ (d, w) ∈ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r
Tactic:
simp only [mem_inter_iff, mem_prod_eq, mem_image, @mem_ball _ _ c, lt_min_iff] at m op ⊢
Proof state after:
case right
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ w ∈ ball (f c z) (e / 4)
⊢ ∃ x, (x.1 ∈ u ∧ x.2 ∈ closedBall z r) ∧ (x.1, f x.1 x.2) = (d, w)
Theorem: AnalyticOn.ball_subset_image_closedBall_param
Proof state before:
case right
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ w ∈ ball (f c z) (e / 4)
⊢ ∃ x, (x.1 ∈ u ∧ x.2 ∈ closedBall z r) ∧ (x.1, f x.1 x.2) = (d, w)
Tactic:
have wm : w ∈ ball (f d z) (e / 2) := by
  simp only [mem_ball] at m ⊢
  specialize @sh ⟨d, z⟩; simp only [Prod.dist_eq, dist_self, Function.uncurry] at sh
  specialize sh (max_lt m.1.2 sp); rw [dist_comm] at sh
  calc dist w (f d z)
    _ ≤ dist w (f c z) + dist (f c z) (f d z) := by bound
    _ < e / 4 + dist (f c z) (f d z) := by linarith [m.2]
    _ ≤ e / 4 + e / 4 := by linarith [sh]
    _ = e / 2 := by ring
Proof state after:
case right
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ w ∈ ball (f c z) (e / 4)
wm : w ∈ ball (f d z) (e / 2)
⊢ ∃ x, (x.1 ∈ u ∧ x.2 ∈ closedBall z r) ∧ (x.1, f x.1 x.2) = (d, w)
Theorem: AnalyticOn.ball_subset_image_closedBall_param
Proof state before:
case right
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ w ∈ ball (f c z) (e / 4)
wm : w ∈ ball (f d z) (e / 2)
⊢ ∃ x, (x.1 ∈ u ∧ x.2 ∈ closedBall z r) ∧ (x.1, f x.1 x.2) = (d, w)
Tactic:
specialize op d m.1.1 wm
Proof state after:
case right
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ w ∈ ball (f c z) (e / 4)
wm : w ∈ ball (f d z) (e / 2)
op : w ∈ f d '' closedBall z r
⊢ ∃ x, (x.1 ∈ u ∧ x.2 ∈ closedBall z r) ∧ (x.1, f x.1 x.2) = (d, w)
Theorem: AnalyticOn.ball_subset_image_closedBall_param
Proof state before:
case right
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ w ∈ ball (f c z) (e / 4)
wm : w ∈ ball (f d z) (e / 2)
op : w ∈ f d '' closedBall z r
⊢ ∃ x, (x.1 ∈ u ∧ x.2 ∈ closedBall z r) ∧ (x.1, f x.1 x.2) = (d, w)
Tactic:
rcases (mem_image _ _ _).mp op with ⟨y, yr, yw⟩
Proof state after:
case right.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ w ∈ ball (f c z) (e / 4)
wm : w ∈ ball (f d z) (e / 2)
op : w ∈ f d '' closedBall z r
y : ℂ
yr : y ∈ closedBall z r
yw : f d y = w
⊢ ∃ x, (x.1 ∈ u ∧ x.2 ∈ closedBall z r) ∧ (x.1, f x.1 x.2) = (d, w)