Theorem: NontrivialHolomorphicAt.on_preconnected (Ray/AnalyticManifold/Nontrivial.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✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
s : Set S
z : S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
n : NontrivialHolomorphicAt f z
⊢ NontrivialHolomorphicOn f s
Tactic:
intro w ws
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✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
s : Set S
z : S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
n : NontrivialHolomorphicAt f z
w : S
ws : w ∈ s
⊢ NontrivialHolomorphicAt f w

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✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
s : Set S
z : S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
n : NontrivialHolomorphicAt f z
w : S
ws : w ∈ s
⊢ NontrivialHolomorphicAt f w
Tactic:
replace n := n.nonconst
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✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
s : Set S
z : S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
w : S
ws : w ∈ s
n : ∃ᶠ (w : S) in 𝓝 z, f w ≠ f z
⊢ NontrivialHolomorphicAt f w

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✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
s : Set S
z : S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
w : S
ws : w ∈ s
n : ∃ᶠ (w : S) in 𝓝 z, f w ≠ f z
⊢ NontrivialHolomorphicAt f w
Tactic:
refine ⟨fa _ ws, ?_⟩
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✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
s : Set S
z : S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
w : S
ws : w ∈ s
n : ∃ᶠ (w : S) in 𝓝 z, f w ≠ f z
⊢ ∃ᶠ (w_1 : S) in 𝓝 w, f w_1 ≠ f w

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✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
s : Set S
z : S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
w : S
ws : w ∈ s
n : ∃ᶠ (w : S) in 𝓝 z, f w ≠ f z
⊢ ∃ᶠ (w_1 : S) in 𝓝 w, f w_1 ≠ f w
Tactic:
contrapose n
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✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
s : Set S
z : S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
w : S
ws : w ∈ s
n : ¬∃ᶠ (w_1 : S) in 𝓝 w, f w_1 ≠ f w
⊢ ¬∃ᶠ (w : S) in 𝓝 z, f w ≠ 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✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
s : Set S
z : S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
w : S
ws : w ∈ s
n : ¬∃ᶠ (w_1 : S) in 𝓝 w, f w_1 ≠ f w
⊢ ¬∃ᶠ (w : S) in 𝓝 z, f w ≠ f z
Tactic:
simp only [Filter.not_frequently, not_not] at n ⊢
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✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
s : Set S
z : S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
w : S
ws : w ∈ s
n : ∀ᶠ (x : S) in 𝓝 w, f x = f w
⊢ ∀ᶠ (x : S) in 𝓝 z, f x = 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✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
s : Set S
z : S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
w : S
ws : w ∈ s
n : ∀ᶠ (x : S) in 𝓝 w, f x = f w
⊢ ∀ᶠ (x : S) in 𝓝 z, f x = f z
Tactic:
generalize ha : f w = a
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✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
s : Set S
z : S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
w : S
ws : w ∈ s
n : ∀ᶠ (x : S) in 𝓝 w, f x = f w
a : T
ha : f w = a
⊢ ∀ᶠ (x : S) in 𝓝 z, f x = 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✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
s : Set S
z : S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
w : S
ws : w ∈ s
n : ∀ᶠ (x : S) in 𝓝 w, f x = f w
a : T
ha : f w = a
⊢ ∀ᶠ (x : S) in 𝓝 z, f x = f z
Tactic:
rw [ha] at n
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✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
s : Set S
z : S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
w : S
ws : w ∈ s
a : T
n : ∀ᶠ (x : S) in 𝓝 w, f x = a
ha : f w = a
⊢ ∀ᶠ (x : S) in 𝓝 z, f x = 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✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
s : Set S
z : S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
w : S
ws : w ∈ s
a : T
n : ∀ᶠ (x : S) in 𝓝 w, f x = a
ha : f w = a
⊢ ∀ᶠ (x : S) in 𝓝 z, f x = f z
Tactic:
rw [eventually_nhds_iff]
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✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
s : Set S
z : S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
w : S
ws : w ∈ s
a : T
n : ∀ᶠ (x : S) in 𝓝 w, f x = a
ha : f w = a
⊢ ∃ t, (∀ x ∈ t, f x = f z) ∧ IsOpen t ∧ z ∈ t

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✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
s : Set S
z : S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
w : S
ws : w ∈ s
a : T
n : ∀ᶠ (x : S) in 𝓝 w, f x = a
ha : f w = a
⊢ ∃ t, (∀ x ∈ t, f x = f z) ∧ IsOpen t ∧ z ∈ t
Tactic:
refine ⟨s, ?_, o, zs⟩
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✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
s : Set S
z : S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
w : S
ws : w ∈ s
a : T
n : ∀ᶠ (x : S) in 𝓝 w, f x = a
ha : f w = a
⊢ ∀ x ∈ s, f x = 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✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
s : Set S
z : S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
w : S
ws : w ∈ s
a : T
n : ∀ᶠ (x : S) in 𝓝 w, f x = a
ha : f w = a
⊢ ∀ x ∈ s, f x = f z
Tactic:
have c := fa.const_of_locally_const ws o p n
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✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
s : Set S
z : S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
w : S
ws : w ∈ s
a : T
n : ∀ᶠ (x : S) in 𝓝 w, f x = a
ha : f w = a
c : ∀ w ∈ s, f w = a
⊢ ∀ x ∈ s, f x = 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✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
s : Set S
z : S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
w : S
ws : w ∈ s
a : T
n : ∀ᶠ (x : S) in 𝓝 w, f x = a
ha : f w = a
c : ∀ w ∈ s, f w = a
⊢ ∀ x ∈ s, f x = f z
Tactic:
intro x m
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✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
s : Set S
z : S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
w : S
ws : w ∈ s
a : T
n : ∀ᶠ (x : S) in 𝓝 w, f x = a
ha : f w = a
c : ∀ w ∈ s, f w = a
x : S
m : x ∈ s
⊢ f x = 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✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
s : Set S
z : S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
w : S
ws : w ∈ s
a : T
n : ∀ᶠ (x : S) in 𝓝 w, f x = a
ha : f w = a
c : ∀ w ∈ s, f w = a
x : S
m : x ∈ s
⊢ f x = f z
Tactic:
rw [c _ m, c _ zs]
State after:
no goals