internlm/Lean-Github huggingface dataset:
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case neg.inr.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✝ : ℂ → ℂ
s : Set ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
gc : ContinuousAt g z
fg : f z = g z
x : S
xm : x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) z).source
gm : g x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source
fm : f x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source
xz : x ≠ z
h :
  ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z →
    ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f x) ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (g x)
⊢ f x ≠ g x
Tactic:
specialize h ((PartialEquiv.injOn _).ne xm (mem_extChartAt_source _ _) xz)
Proof state after:
case neg.inr.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✝ : ℂ → ℂ
s : Set ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
gc : ContinuousAt g z
fg : f z = g z
x : S
xm : x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) z).source
gm : g x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source
fm : f x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source
xz : x ≠ z
h : ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f x) ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (g x)
⊢ f x ≠ g x
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case neg.inr.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✝ : ℂ → ℂ
s : Set ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
gc : ContinuousAt g z
fg : f z = g z
x : S
xm : x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) z).source
gm : g x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source
fm : f x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source
xz : x ≠ z
h : ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f x) ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (g x)
⊢ f x ≠ g x
Tactic:
rwa [← (PartialEquiv.injOn _).ne_iff fm gm]
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✝ : 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
⊢ ∀ w ∈ s, f w = a
Tactic:
generalize ht : {z | z ∈ s ∧ ∀ᶠ w in 𝓝 z, f w = a} = t
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
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
⊢ ∀ w ∈ s, f w = a
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✝ : 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
⊢ ∀ w ∈ s, f w = a
Tactic:
suffices st : s ⊆ t by rw [← ht] at st; exact fun z m ↦ (st m).2.self_of_nhds
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
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
⊢ s ⊆ t
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✝ : 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
⊢ s ⊆ t
Tactic:
refine p.subset_of_closure_inter_subset ?_ ?_ ?_
Proof state after:
case 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✝ : ℂ → ℂ
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
⊢ IsOpen t

case 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✝ : ℂ → ℂ
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
⊢ (s ∩ t).Nonempty

case refine_3
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
⊢ closure t ∩ s ⊆ t
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✝ : 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
st : s ⊆ t
⊢ ∀ w ∈ s, f w = a
Tactic:
rw [← ht] at st
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
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
st : s ⊆ {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a}
⊢ ∀ w ∈ s, f w = a
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✝ : 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
st : s ⊆ {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a}
⊢ ∀ w ∈ s, f w = a
Tactic:
exact fun z m ↦ (st m).2.self_of_nhds
Proof state after:
no goals
Theorem: HolomorphicOn.const_of_locally_const
Proof state before:
case 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✝ : ℂ → ℂ
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
⊢ IsOpen t
Tactic:
rw [isOpen_iff_eventually]
Proof state after:
case 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✝ : ℂ → ℂ
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
⊢ ∀ x ∈ t, ∀ᶠ (y : S) in 𝓝 x, y ∈ t
Theorem: HolomorphicOn.const_of_locally_const
Proof state before:
case 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✝ : ℂ → ℂ
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
⊢ ∀ x ∈ t, ∀ᶠ (y : S) in 𝓝 x, y ∈ t
Tactic:
intro z m
Proof state after:
case 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✝ : ℂ → ℂ
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 : z ∈ t
⊢ ∀ᶠ (y : S) in 𝓝 z, y ∈ t
Theorem: HolomorphicOn.const_of_locally_const
Proof state before:
case 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✝ : ℂ → ℂ
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 : z ∈ t
⊢ ∀ᶠ (y : S) in 𝓝 z, y ∈ t
Tactic:
simp only [Set.mem_setOf_eq, ← ht] at m ⊢
Proof state after:
case 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✝ : ℂ → ℂ
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 : z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a
⊢ ∀ᶠ (y : S) in 𝓝 z, y ∈ s ∧ ∀ᶠ (w : S) in 𝓝 y, f w = a
Theorem: HolomorphicOn.const_of_locally_const
Proof state before:
case 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✝ : ℂ → ℂ
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 : z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a
⊢ ∀ᶠ (y : S) in 𝓝 z, y ∈ s ∧ ∀ᶠ (w : S) in 𝓝 y, f w = a
Tactic:
exact ((o.eventually_mem m.1).and m.2.eventually_nhds).mp (eventually_of_forall fun y h ↦ h)
Proof state after:
no goals
Theorem: HolomorphicOn.const_of_locally_const
Proof state before:
case 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✝ : ℂ → ℂ
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
⊢ (s ∩ t).Nonempty
Tactic:
use z
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✝ : ℂ → ℂ
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 ∩ t
Theorem: HolomorphicOn.const_of_locally_const
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✝ : ℂ → ℂ
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 ∩ t
Tactic:
simp only [Set.mem_inter_iff, ← ht]
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✝ : ℂ → ℂ
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 ∧ z ∈ {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a}
Theorem: HolomorphicOn.const_of_locally_const
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✝ : ℂ → ℂ
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 ∧ z ∈ {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a}
Tactic:
exact ⟨zs, zs, c⟩
Proof state after:
no goals
Theorem: HolomorphicOn.const_of_locally_const
Proof state before:
case refine_3
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
⊢ closure t ∩ s ⊆ t
Tactic:
intro z m
Proof state after:
case refine_3
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 : z ∈ closure t ∩ s
⊢ z ∈ t
Theorem: HolomorphicOn.const_of_locally_const
Proof state before:
case refine_3
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 : z ∈ closure t ∩ s
⊢ z ∈ t
Tactic:
simp only [Set.mem_inter_iff, mem_closure_iff_frequently] at m
Proof state after:
case refine_3
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
⊢ z ∈ t
Theorem: HolomorphicOn.const_of_locally_const
Proof state before:
case refine_3
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
⊢ z ∈ t
Tactic:
have aa : HolomorphicAt I I (fun _ ↦ a) z := holomorphicAt_const
Proof state after:
case refine_3
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
⊢ z ∈ t