Theorem: nontrivial_local_of_global (Ray/AnalyticManifold/OpenMapping.lean)

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
ef : ∀ w ∈ sphere z r, e ≤ ‖f w - f z‖
⊢ NontrivialHolomorphicAt f z
Tactic:
have fh : HolomorphicOn I I f (closedBall z r) := fun _ m ↦ (fa _ m).holomorphicAt I I
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 : ℂ → ℂ
z : ℂ
e r : ℝ
fa : AnalyticOn ℂ f (closedBall z r)
rp : 0 < r
ep : 0 < e
ef : ∀ w ∈ sphere z r, e ≤ ‖f w - f z‖
fh : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (closedBall z r)
⊢ NontrivialHolomorphicAt f z

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
ef : ∀ w ∈ sphere z r, e ≤ ‖f w - f z‖
fh : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (closedBall z r)
⊢ NontrivialHolomorphicAt f z
Tactic:
have zs : z ∈ closedBall z r := mem_closedBall_self rp.le
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 : ℂ → ℂ
z : ℂ
e r : ℝ
fa : AnalyticOn ℂ f (closedBall z r)
rp : 0 < r
ep : 0 < e
ef : ∀ w ∈ sphere z r, e ≤ ‖f w - f z‖
fh : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (closedBall z r)
zs : z ∈ closedBall z r
⊢ NontrivialHolomorphicAt f z

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
ef : ∀ w ∈ sphere z r, e ≤ ‖f w - f z‖
fh : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (closedBall z r)
zs : z ∈ closedBall z r
⊢ NontrivialHolomorphicAt f z
Tactic:
use fh _ zs
State after:
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
ef : ∀ w ∈ sphere z r, e ≤ ‖f w - f z‖
fh : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (closedBall z r)
zs : z ∈ closedBall z r
⊢ ∃ᶠ (w : ℂ) in 𝓝 z, f w ≠ f z

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
ef : ∀ w ∈ sphere z r, e ≤ ‖f w - f z‖
fh : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (closedBall z r)
zs : z ∈ closedBall z r
⊢ ∃ᶠ (w : ℂ) in 𝓝 z, f w ≠ f z
Tactic:
contrapose ef
State after:
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 : ¬∃ᶠ (w : ℂ) in 𝓝 z, f w ≠ f z
⊢ ¬∀ w ∈ sphere z r, e ≤ ‖f w - f z‖

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 : ¬∃ᶠ (w : ℂ) in 𝓝 z, f w ≠ f z
⊢ ¬∀ w ∈ sphere z r, e ≤ ‖f w - f z‖
Tactic:
simp only [Filter.not_frequently, not_not] at ef
State after:
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
⊢ ¬∀ w ∈ sphere z r, e ≤ ‖f w - f z‖

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
⊢ ¬∀ w ∈ sphere z r, e ≤ ‖f w - f z‖
Tactic:
simp only [not_forall, not_le]
State after:
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
⊢ ∃ x, ∃ (_ : x ∈ sphere z r), ‖f x - f z‖ < e

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
⊢ ∃ x, ∃ (_ : x ∈ sphere z r), ‖f x - f z‖ < e
Tactic:
have zrs : z + r ∈ sphere z r := by
  simp only [mem_sphere, Complex.dist_eq, add_sub_cancel_left, Complex.abs_ofReal, abs_of_pos rp]
State after:
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

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
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

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]
State after:
no goals

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]
State after:
no goals