internlm/Lean-Github huggingface dataset:
Theorem: HolomorphicOn.const_of_locally_const
Proof state before:
case neg
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
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
m' : ¬z ∈ t
x : S
xz : ¬x = z
i : ¬x ∉ t
⊢ ¬f x ≠ a
Tactic:
simp only [not_not, ← ht] at i ⊢
Proof state after:
case neg
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
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
m' : ¬z ∈ t
x : S
xz : ¬x = z
i : x ∈ {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a}
⊢ f x = a
Theorem: HolomorphicOn.const_of_locally_const
Proof state before:
case neg
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
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
m' : ¬z ∈ t
x : S
xz : ¬x = z
i : x ∈ {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a}
⊢ f x = a
Tactic:
exact i.2.self_of_nhds
Proof state after:
no goals
Theorem: HolomorphicOn.const_of_locally_const'
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✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝¹ : LocallyConnectedSpace S
inst✝ : T2Space T
f : S → T
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z : S
a : T
zs : z ∈ s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z, f w = a
⊢ ∀ w ∈ s, f w = a
Tactic:
rcases local_preconnected_nhdsSet p (isOpen_holomorphicAt.mem_nhdsSet.mpr fa)
  with ⟨u, uo, su, ua, uc⟩
Proof state after:
case 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✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝¹ : LocallyConnectedSpace S
inst✝ : T2Space T
f : S → T
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z : S
a : T
zs : z ∈ s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z, f w = a
u : Set S
uo : IsOpen u
su : s ⊆ u
ua : u ⊆ {x | HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f x}
uc : IsPreconnected u
⊢ ∀ w ∈ s, f w = a
Theorem: HolomorphicOn.const_of_locally_const'
Proof state before:
case 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✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝¹ : LocallyConnectedSpace S
inst✝ : T2Space T
f : S → T
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z : S
a : T
zs : z ∈ s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z, f w = a
u : Set S
uo : IsOpen u
su : s ⊆ u
ua : u ⊆ {x | HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f x}
uc : IsPreconnected u
⊢ ∀ w ∈ s, f w = a
Tactic:
exact fun w ws ↦ HolomorphicOn.const_of_locally_const (fun _ m ↦ ua m) (su zs) uo uc c w (su ws)
Proof state after:
no goals
Theorem: NontrivialHolomorphicAt.eventually_ne
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✝ : ℂ → ℂ
s : Set ℂ
inst✝ : T2Space T
f : S → T
z : S
n : NontrivialHolomorphicAt f z
⊢ ∀ᶠ (w : S) in 𝓝 z, w ≠ z → f w ≠ f z
Tactic:
have ca : _root_.HolomorphicAt I I (fun _ ↦ f z) z := holomorphicAt_const
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✝ : ℂ → ℂ
s : Set ℂ
inst✝ : T2Space T
f : S → T
z : S
n : NontrivialHolomorphicAt f z
ca : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => f z) z
⊢ ∀ᶠ (w : S) in 𝓝 z, w ≠ z → f w ≠ f z
Theorem: NontrivialHolomorphicAt.eventually_ne
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✝ : ℂ → ℂ
s : Set ℂ
inst✝ : T2Space T
f : S → T
z : S
n : NontrivialHolomorphicAt f z
ca : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => f z) z
⊢ ∀ᶠ (w : S) in 𝓝 z, w ≠ z → f w ≠ f z
Tactic:
cases' n.holomorphicAt.eventually_eq_or_eventually_ne ca with h h
Proof state after:
case inl
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
z : S
n : NontrivialHolomorphicAt f z
ca : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => f z) z
h : ∀ᶠ (w : S) in 𝓝 z, f w = f z
⊢ ∀ᶠ (w : S) in 𝓝 z, w ≠ z → f w ≠ f z

case inr
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
z : S
n : NontrivialHolomorphicAt f z
ca : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => f z) z
h : ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ f z
⊢ ∀ᶠ (w : S) in 𝓝 z, w ≠ z → f w ≠ f z
Theorem: NontrivialHolomorphicAt.eventually_ne
Proof state before:
case inl
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
z : S
n : NontrivialHolomorphicAt f z
ca : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => f z) z
h : ∀ᶠ (w : S) in 𝓝 z, f w = f z
⊢ ∀ᶠ (w : S) in 𝓝 z, w ≠ z → f w ≠ f z
Tactic:
have b := h.and_frequently n.nonconst
Proof state after:
case inl
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
z : S
n : NontrivialHolomorphicAt f z
ca : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => f z) z
h : ∀ᶠ (w : S) in 𝓝 z, f w = f z
b : ∃ᶠ (x : S) in 𝓝 z, f x = f z ∧ f x ≠ f z
⊢ ∀ᶠ (w : S) in 𝓝 z, w ≠ z → f w ≠ f z
Theorem: NontrivialHolomorphicAt.eventually_ne
Proof state before:
case inl
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
z : S
n : NontrivialHolomorphicAt f z
ca : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => f z) z
h : ∀ᶠ (w : S) in 𝓝 z, f w = f z
b : ∃ᶠ (x : S) in 𝓝 z, f x = f z ∧ f x ≠ f z
⊢ ∀ᶠ (w : S) in 𝓝 z, w ≠ z → f w ≠ f z
Tactic:
simp only [and_not_self_iff, Filter.frequently_false] at b
Proof state after:
no goals
Theorem: NontrivialHolomorphicAt.eventually_ne
Proof state before:
case inr
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
z : S
n : NontrivialHolomorphicAt f z
ca : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => f z) z
h : ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ f z
⊢ ∀ᶠ (w : S) in 𝓝 z, w ≠ z → f w ≠ f z
Tactic:
simp only [eventually_nhdsWithin_iff, mem_compl_singleton_iff] at h
Proof state after:
case inr
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
z : S
n : NontrivialHolomorphicAt f z
ca : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => f z) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ f z
⊢ ∀ᶠ (w : S) in 𝓝 z, w ≠ z → f w ≠ f z
Theorem: NontrivialHolomorphicAt.eventually_ne
Proof state before:
case inr
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
z : S
n : NontrivialHolomorphicAt f z
ca : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => f z) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ f z
⊢ ∀ᶠ (w : S) in 𝓝 z, w ≠ z → f w ≠ f z
Tactic:
convert h
Proof state after:
no goals
Theorem: NontrivialHolomorphicAt.on_preconnected
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✝ : ℂ → ℂ
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
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✝ : ℂ → ℂ
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
Theorem: NontrivialHolomorphicAt.on_preconnected
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✝ : ℂ → ℂ
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
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✝ : ℂ → ℂ
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
Theorem: NontrivialHolomorphicAt.on_preconnected
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✝ : ℂ → ℂ
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, ?_⟩
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✝ : ℂ → ℂ
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
Theorem: NontrivialHolomorphicAt.on_preconnected
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✝ : ℂ → ℂ
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
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✝ : ℂ → ℂ
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
Theorem: NontrivialHolomorphicAt.on_preconnected
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✝ : ℂ → ℂ
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 ⊢
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✝ : ℂ → ℂ
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
Theorem: NontrivialHolomorphicAt.on_preconnected
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✝ : ℂ → ℂ
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
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✝ : ℂ → ℂ
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
Theorem: NontrivialHolomorphicAt.on_preconnected
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✝ : ℂ → ℂ
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
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✝ : ℂ → ℂ
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
Theorem: NontrivialHolomorphicAt.on_preconnected
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✝ : ℂ → ℂ
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]
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✝ : ℂ → ℂ
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
Theorem: NontrivialHolomorphicAt.on_preconnected
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✝ : ℂ → ℂ
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⟩
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✝ : ℂ → ℂ
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
Theorem: NontrivialHolomorphicAt.on_preconnected
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✝ : ℂ → ℂ
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
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✝ : ℂ → ℂ
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