internlm/Lean-Github huggingface dataset:
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) ∧ dist w (f c z) < e / 4
⊢ dist w (f d z) < e / 2
Tactic:
specialize @sh ⟨d, z⟩
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
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ dist w (f c z) < e / 4
sh : dist (d, z) (c, z) < s → dist (uncurry f (d, z)) (uncurry f (c, z)) < e / 4
⊢ dist w (f d z) < e / 2
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
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ dist w (f c z) < e / 4
sh : dist (d, z) (c, z) < s → dist (uncurry f (d, z)) (uncurry f (c, z)) < e / 4
⊢ dist w (f d z) < e / 2
Tactic:
simp only [Prod.dist_eq, dist_self, Function.uncurry] at sh
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
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ dist w (f c z) < e / 4
sh : max (dist d c) 0 < s → dist (f d z) (f c z) < e / 4
⊢ dist w (f d z) < e / 2
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
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ dist w (f c z) < e / 4
sh : max (dist d c) 0 < s → dist (f d z) (f c z) < e / 4
⊢ dist w (f d z) < e / 2
Tactic:
specialize sh (max_lt m.1.2 sp)
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
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ dist w (f c z) < e / 4
sh : dist (f d z) (f c z) < e / 4
⊢ dist w (f d z) < e / 2
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
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ dist w (f c z) < e / 4
sh : dist (f d z) (f c z) < e / 4
⊢ dist w (f d z) < e / 2
Tactic:
rw [dist_comm] at sh
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
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ dist w (f c z) < e / 4
sh : dist (f c z) (f d z) < e / 4
⊢ dist w (f d z) < e / 2
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
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ dist w (f c z) < e / 4
sh : dist (f c z) (f d z) < e / 4
⊢ dist w (f d z) < e / 2
Tactic:
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:
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
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ dist w (f c z) < e / 4
sh : dist (f c z) (f d z) < e / 4
⊢ dist w (f d z) ≤ dist w (f c z) + dist (f c z) (f d z)
Tactic:
bound
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
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ dist w (f c z) < e / 4
sh : dist (f c z) (f d z) < e / 4
⊢ dist w (f c z) + dist (f c z) (f d z) < e / 4 + dist (f c z) (f d z)
Tactic:
linarith [m.2]
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
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ dist w (f c z) < e / 4
sh : dist (f c z) (f d z) < e / 4
⊢ e / 4 + dist (f c z) (f d z) ≤ e / 4 + e / 4
Tactic:
linarith [sh]
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
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ dist w (f c z) < e / 4
sh : dist (f c z) (f d z) < e / 4
⊢ e / 4 + e / 4 = e / 2
Tactic:
ring
Proof state after:
no goals
Theorem: abs_sub_self_lt
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
z : ℂ
r : ℝ
rp : 0 < r
⊢ Complex.abs (z - z) < r
Tactic:
simp [sub_self, Complex.abs.map_zero, rp]
Proof state after:
no goals
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_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 : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
⊢ 𝓝 (c, f c z) ≤ Filter.map (fun p => (p.1, f p.1 p.2)) (𝓝 (c, z))
Tactic:
rw [Filter.le_map_iff]
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 : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
⊢ ∀ s ∈ 𝓝 (c, z), (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_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 : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
⊢ ∀ s ∈ 𝓝 (c, z), (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)
Tactic:
intro s' sn
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 : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
s' : Set (ℂ × ℂ)
sn : s' ∈ 𝓝 (c, z)
⊢ (fun p => (p.1, f p.1 p.2)) '' s' ∈ 𝓝 (c, f c z)
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_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 : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
s' : Set (ℂ × ℂ)
sn : s' ∈ 𝓝 (c, z)
⊢ (fun p => (p.1, f p.1 p.2)) '' s' ∈ 𝓝 (c, f c z)
Tactic:
generalize hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
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 : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
s' : Set (ℂ × ℂ)
sn : s' ∈ 𝓝 (c, z)
s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
⊢ (fun p => (p.1, f p.1 p.2)) '' s' ∈ 𝓝 (c, f c z)
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_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 : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
s' : Set (ℂ × ℂ)
sn : s' ∈ 𝓝 (c, z)
s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
⊢ (fun p => (p.1, f p.1 p.2)) '' s' ∈ 𝓝 (c, f c z)
Tactic:
have ss : s ⊆ s' := by rw [← hs]; apply inter_subset_left
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 : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
s' : Set (ℂ × ℂ)
sn : s' ∈ 𝓝 (c, z)
s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
ss : s ⊆ s'
⊢ (fun p => (p.1, f p.1 p.2)) '' s' ∈ 𝓝 (c, f c z)
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_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 : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
s' : Set (ℂ × ℂ)
sn : s' ∈ 𝓝 (c, z)
s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
ss : s ⊆ s'
⊢ (fun p => (p.1, f p.1 p.2)) '' s' ∈ 𝓝 (c, f c z)
Tactic:
replace sn : s ∈ 𝓝 (c, z) := by rw [← hs]; exact Filter.inter_mem sn fa.eventually_analyticAt
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 : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
s' s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
ss : s ⊆ s'
sn : s ∈ 𝓝 (c, z)
⊢ (fun p => (p.1, f p.1 p.2)) '' s' ∈ 𝓝 (c, f c z)
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_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 : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
s' s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
ss : s ⊆ s'
sn : s ∈ 𝓝 (c, z)
⊢ (fun p => (p.1, f p.1 p.2)) '' s' ∈ 𝓝 (c, f c z)
Tactic:
replace fa : AnalyticOn ℂ (uncurry f) s := by rw [← hs]; apply inter_subset_right
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 : ℂ
n : NontrivialHolomorphicAt (f c) z
s' s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
ss : s ⊆ s'
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
⊢ (fun p => (p.1, f p.1 p.2)) '' s' ∈ 𝓝 (c, f c z)
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_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 : ℂ
n : NontrivialHolomorphicAt (f c) z
s' s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
ss : s ⊆ s'
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
⊢ (fun p => (p.1, f p.1 p.2)) '' s' ∈ 𝓝 (c, f c z)
Tactic:
refine Filter.mem_of_superset ?_ (image_subset _ ss)
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 : ℂ
n : NontrivialHolomorphicAt (f c) z
s' s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
ss : s ⊆ s'
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_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 : ℂ
n : NontrivialHolomorphicAt (f c) z
s' s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
ss : s ⊆ s'
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)
Tactic:
clear ss hs s'
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 : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_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 : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)
Tactic:
rcases Metric.mem_nhds_iff.mp sn with ⟨e, ep, es⟩
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 : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_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 : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
er : ∃ r, 0 < r ∧ closedBall (c, z) r ⊆ s ∧ f c z ∉ f c '' sphere z r
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)
Tactic:
rcases er with ⟨r, rp, rs, fr⟩
Proof state after:
case intro.intro.intro.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 : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)