internlm/Lean-Github huggingface dataset:
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
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
h : ∀ (x : ℝ), 0 < x → closedBall (c, z) x ⊆ s → f c z ∈ f c '' sphere z x
⊢ ¬∀ᶠ (w : ℂ) in 𝓝 z, w ≠ z → f c w ≠ f c z
Tactic:
simp only [Filter.not_eventually, _root_.not_imp, not_not, Filter.eventually_iff,
  Metric.mem_nhds_iff, not_exists, not_subset, mem_setOf, not_and]
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
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
h : ∀ (x : ℝ), 0 < x → closedBall (c, z) x ⊆ s → f c z ∈ f c '' sphere z x
⊢ ∀ x > 0, ∃ a ∈ ball z x, a ≠ z ∧ f c a = 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
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
h : ∀ (x : ℝ), 0 < x → closedBall (c, z) x ⊆ s → f c z ∈ f c '' sphere z x
⊢ ∀ x > 0, ∃ a ∈ ball z x, a ≠ z ∧ f c a = f c z
Tactic:
intro r rp
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
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
h : ∀ (x : ℝ), 0 < x → closedBall (c, z) x ⊆ s → f c z ∈ f c '' sphere z x
r : ℝ
rp : r > 0
⊢ ∃ a ∈ ball z r, a ≠ z ∧ f c a = 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
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
h : ∀ (x : ℝ), 0 < x → closedBall (c, z) x ⊆ s → f c z ∈ f c '' sphere z x
r : ℝ
rp : r > 0
⊢ ∃ a ∈ ball z r, a ≠ z ∧ f c a = f c z
Tactic:
specialize h (min (e/2) (r/2)) ?_ ?_
Proof state after:
case specialize_1
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
h : ∀ (x : ℝ), 0 < x → closedBall (c, z) x ⊆ s → f c z ∈ f c '' sphere z x
r : ℝ
rp : r > 0
⊢ 0 < min (e / 2) (r / 2)

case specialize_2
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
h : ∀ (x : ℝ), 0 < x → closedBall (c, z) x ⊆ s → f c z ∈ f c '' sphere z x
r : ℝ
rp : r > 0
⊢ closedBall (c, z) (min (e / 2) (r / 2)) ⊆ s

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 : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
⊢ ∃ a ∈ ball z r, a ≠ z ∧ f c a = f c z
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_param'
Proof state before:
case specialize_1
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
h : ∀ (x : ℝ), 0 < x → closedBall (c, z) x ⊆ s → f c z ∈ f c '' sphere z x
r : ℝ
rp : r > 0
⊢ 0 < min (e / 2) (r / 2)
Tactic:
bound
Proof state after:
no goals
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_param'
Proof state before:
case specialize_2
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
h : ∀ (x : ℝ), 0 < x → closedBall (c, z) x ⊆ s → f c z ∈ f c '' sphere z x
r : ℝ
rp : r > 0
⊢ closedBall (c, z) (min (e / 2) (r / 2)) ⊆ s
Tactic:
exact _root_.trans (Metric.closedBall_subset_ball (lt_of_le_of_lt (min_le_left _ _)
  (half_lt_self ep))) es
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
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
⊢ ∃ a ∈ ball z r, a ≠ z ∧ f c a = f c z
Tactic:
rcases (mem_image _ _ _).mp h with ⟨w, ws, wz⟩
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
r : ℝ
rp : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
ws : w ∈ sphere z (min (e / 2) (r / 2))
wz : f c w = f c z
⊢ ∃ a ∈ ball z r, a ≠ z ∧ f c a = 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
r : ℝ
rp : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
ws : w ∈ sphere z (min (e / 2) (r / 2))
wz : f c w = f c z
⊢ ∃ a ∈ ball z r, a ≠ z ∧ f c a = f c z
Tactic:
use w
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 : ℂ
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 : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
ws : w ∈ sphere z (min (e / 2) (r / 2))
wz : f c w = f c z
⊢ w ∈ ball z r ∧ w ≠ z ∧ f c w = f c z
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_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 : ℂ
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 : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
ws : w ∈ sphere z (min (e / 2) (r / 2))
wz : f c w = f c z
⊢ w ∈ ball z r ∧ w ≠ z ∧ f c w = f c z
Tactic:
refine ⟨?_, ?_, wz⟩
Proof state after:
case h.refine_1
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 : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
ws : w ∈ sphere z (min (e / 2) (r / 2))
wz : f c w = f c z
⊢ w ∈ ball z r

case h.refine_2
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 : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
ws : w ∈ sphere z (min (e / 2) (r / 2))
wz : f c w = f c z
⊢ w ≠ z
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_param'
Proof state before:
case h.refine_1
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 : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
ws : w ∈ sphere z (min (e / 2) (r / 2))
wz : f c w = f c z
⊢ w ∈ ball z r
Tactic:
exact Metric.closedBall_subset_ball (lt_of_le_of_lt (min_le_right _ _) (half_lt_self rp))
  (Metric.sphere_subset_closedBall ws)
Proof state after:
no goals
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_param'
Proof state before:
case h.refine_2
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 : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
ws : w ∈ sphere z (min (e / 2) (r / 2))
wz : f c w = f c z
⊢ w ≠ z
Tactic:
contrapose ws
Proof state after:
case h.refine_2
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 : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
wz : f c w = f c z
ws : ¬w ≠ z
⊢ w ∉ sphere z (min (e / 2) (r / 2))
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_param'
Proof state before:
case h.refine_2
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 : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
wz : f c w = f c z
ws : ¬w ≠ z
⊢ w ∉ sphere z (min (e / 2) (r / 2))
Tactic:
simp only [not_not] at ws
Proof state after:
case h.refine_2
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 : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
wz : f c w = f c z
ws : w = z
⊢ w ∉ sphere z (min (e / 2) (r / 2))
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_param'
Proof state before:
case h.refine_2
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 : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
wz : f c w = f c z
ws : w = z
⊢ w ∉ sphere z (min (e / 2) (r / 2))
Tactic:
simp only [ws, Metric.mem_sphere, dist_self]
Proof state after:
case h.refine_2
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 : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
wz : f c w = f c z
ws : w = z
⊢ ¬0 = min (e / 2) (r / 2)
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_param'
Proof state before:
case h.refine_2
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 : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
wz : f c w = f c z
ws : w = z
⊢ ¬0 = min (e / 2) (r / 2)
Tactic:
exact ne_of_lt (by bound)
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
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
wz : f c w = f c z
ws : w = z
⊢ 0 < min (e / 2) (r / 2)
Tactic:
bound
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
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
⊢ ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
Tactic:
apply ContinuousOn.norm
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 : ℂ
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
⊢ ContinuousOn (fun x => f c x - f c z) (sphere z r)
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_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 : ℂ
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
⊢ ContinuousOn (fun x => f c x - f c z) (sphere z r)
Tactic:
refine ContinuousOn.sub ?_ continuousOn_const
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 : ℂ
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
⊢ ContinuousOn (fun x => f c x) (sphere z r)
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_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 : ℂ
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
⊢ ContinuousOn (fun x => f c x) (sphere z r)
Tactic:
apply fa.along_snd.continuousOn.mono
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 : ℂ
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
⊢ sphere z r ⊆ {y | (c, y) ∈ s}
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_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 : ℂ
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
⊢ sphere z r ⊆ {y | (c, y) ∈ s}
Tactic:
intro x xs
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 : ℂ
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
x : ℂ
xs : x ∈ sphere z r
⊢ x ∈ {y | (c, y) ∈ s}