internlm/Lean-Github huggingface dataset:
Theorem: AnalyticOn.ball_subset_image_closedBall_param
Proof state before:
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)
Tactic:
use⟨d, y⟩
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 : ℂ → ℂ → ℂ
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
⊢ ((d, y).1 ∈ u ∧ (d, y).2 ∈ closedBall z r) ∧ ((d, y).1, f (d, y).1 (d, y).2) = (d, w)
Theorem: AnalyticOn.ball_subset_image_closedBall_param
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 : ℂ → ℂ → ℂ
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
⊢ ((d, y).1 ∈ u ∧ (d, y).2 ∈ closedBall z r) ∧ ((d, y).1, f (d, y).1 (d, y).2) = (d, w)
Tactic:
simp only [mem_prod_eq, Prod.ext_iff, yw, and_true_iff, eq_self_iff_true, true_and_iff, yr, m.1.1]
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‖
⊢ ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
Tactic:
refine fun d m ↦ (nontrivial_local_of_global (fa.along_snd.mono ?_) rp ep (ef d m)).nonconst
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‖
d : ℂ
m : d ∈ u
⊢ closedBall z r ⊆ {y | (d, y) ∈ u ×ˢ closedBall z r}
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‖
d : ℂ
m : d ∈ u
⊢ closedBall z r ⊆ {y | (d, y) ∈ u ×ˢ closedBall z r}
Tactic:
simp only [← closedBall_prod_same, mem_prod_eq, setOf_mem_eq, iff_true_iff.mpr m,
  true_and_iff, subset_refl]
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‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
⊢ ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
Tactic:
intro d 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
d : ℂ
du : d ∈ u
⊢ ball (f d z) (e / 2) ⊆ f d '' closedBall z r
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
d : ℂ
du : d ∈ u
⊢ ball (f d z) (e / 2) ⊆ f d '' closedBall z r
Tactic:
refine DiffContOnCl.ball_subset_image_closedBall ?_ rp (ef d du) (fn d 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
d : ℂ
du : d ∈ u
⊢ DiffContOnCl ℂ (f d) (ball z r)
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
d : ℂ
du : d ∈ u
⊢ DiffContOnCl ℂ (f d) (ball z r)
Tactic:
have e : f d = uncurry f ∘ fun w ↦ (d, w) := rfl
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
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
⊢ DiffContOnCl ℂ (f d) (ball z r)
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
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
⊢ DiffContOnCl ℂ (f d) (ball z r)
Tactic:
rw [e]
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
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
⊢ DiffContOnCl ℂ (uncurry f ∘ fun w => (d, w)) (ball z r)
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
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
⊢ DiffContOnCl ℂ (uncurry f ∘ fun w => (d, w)) (ball z r)
Tactic:
apply DifferentiableOn.diffContOnCl
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 : ℂ → ℂ → ℂ
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
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
⊢ DifferentiableOn ℂ (uncurry f ∘ fun w => (d, w)) (closure (ball z r))
Theorem: AnalyticOn.ball_subset_image_closedBall_param
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 : ℂ → ℂ → ℂ
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
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
⊢ DifferentiableOn ℂ (uncurry f ∘ fun w => (d, w)) (closure (ball z r))
Tactic:
apply AnalyticOn.differentiableOn
Proof state after:
case h.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 : ℂ → ℂ → ℂ
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
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
⊢ AnalyticOn ℂ (uncurry f ∘ fun w => (d, w)) (closure (ball z r))
Theorem: AnalyticOn.ball_subset_image_closedBall_param
Proof state before:
case h.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 : ℂ → ℂ → ℂ
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
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
⊢ AnalyticOn ℂ (uncurry f ∘ fun w => (d, w)) (closure (ball z r))
Tactic:
refine fa.comp (analyticOn_const.prod (analyticOn_id _)) ?_
Proof state after:
case h.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 : ℂ → ℂ → ℂ
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
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
⊢ MapsTo (fun w => (d, w)) (closure (ball z r)) (u ×ˢ closedBall z r)
Theorem: AnalyticOn.ball_subset_image_closedBall_param
Proof state before:
case h.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 : ℂ → ℂ → ℂ
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
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
⊢ MapsTo (fun w => (d, w)) (closure (ball z r)) (u ×ˢ closedBall z r)
Tactic:
intro w wr
Proof state after:
case h.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 : ℂ → ℂ → ℂ
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
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
w : ℂ
wr : w ∈ closure (ball z r)
⊢ (fun w => (d, w)) w ∈ u ×ˢ closedBall z r
Theorem: AnalyticOn.ball_subset_image_closedBall_param
Proof state before:
case h.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 : ℂ → ℂ → ℂ
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
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
w : ℂ
wr : w ∈ closure (ball z r)
⊢ (fun w => (d, w)) w ∈ u ×ˢ closedBall z r
Tactic:
simp only [closure_ball _ rp.ne'] at wr
Proof state after:
case h.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 : ℂ → ℂ → ℂ
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
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
w : ℂ
wr : w ∈ closedBall z r
⊢ (fun w => (d, w)) w ∈ u ×ˢ closedBall z r
Theorem: AnalyticOn.ball_subset_image_closedBall_param
Proof state before:
case h.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 : ℂ → ℂ → ℂ
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
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
w : ℂ
wr : w ∈ closedBall z r
⊢ (fun w => (d, w)) w ∈ u ×ˢ closedBall z r
Tactic:
simp only [← closedBall_prod_same, mem_prod_eq, du, wr, true_and_iff, du]
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‖
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
⊢ e / 4 > 0
Tactic:
linarith
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‖
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
⊢ 0 < s
Tactic:
linarith
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‖
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
⊢ 0 < e / 4
Tactic:
linarith
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‖
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)
⊢ w ∈ ball (f d z) (e / 2)
Tactic:
simp only [mem_ball] at m ⊢
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
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) ∧ dist w (f c z) < e / 4
⊢ dist w (f d z) < e / 2