internlm/Lean-Github huggingface dataset:
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
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
⊢ z ∈ t
Tactic:
cases' (fa _ m.2).eventually_eq_or_eventually_ne aa with h h
Proof state after:
case refine_3.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
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 : ∀ᶠ (w : S) in 𝓝 z, f w = a
⊢ z ∈ t

case refine_3.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
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 : ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ a
⊢ z ∈ t
Theorem: HolomorphicOn.const_of_locally_const
Proof state before:
case refine_3.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
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 : ∀ᶠ (w : S) in 𝓝 z, f w = a
⊢ z ∈ t
Tactic:
rw [← ht]
Proof state after:
case refine_3.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
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 : ∀ᶠ (w : S) in 𝓝 z, f w = a
⊢ z ∈ {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a}
Theorem: HolomorphicOn.const_of_locally_const
Proof state before:
case refine_3.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
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 : ∀ᶠ (w : S) in 𝓝 z, f w = a
⊢ z ∈ {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a}
Tactic:
use m.2, h
Proof state after:
no goals
Theorem: HolomorphicOn.const_of_locally_const
Proof state before:
case refine_3.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
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 : ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ a
⊢ z ∈ t
Tactic:
simp only [eventually_nhdsWithin_iff, Set.mem_compl_singleton_iff] at h
Proof state after:
case refine_3.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
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
⊢ z ∈ t
Theorem: HolomorphicOn.const_of_locally_const
Proof state before:
case refine_3.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
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
⊢ z ∈ t
Tactic:
have m' := m.1
Proof state after:
case refine_3.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
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' : ∃ᶠ (x : S) in 𝓝 z, x ∈ t
⊢ z ∈ t
Theorem: HolomorphicOn.const_of_locally_const
Proof state before:
case refine_3.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
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' : ∃ᶠ (x : S) in 𝓝 z, x ∈ t
⊢ z ∈ t
Tactic:
contrapose m'
Proof state after:
case refine_3.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
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) in 𝓝 z, x ∈ t
Theorem: HolomorphicOn.const_of_locally_const
Proof state before:
case refine_3.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
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) in 𝓝 z, x ∈ t
Tactic:
simp only [Filter.not_frequently]
Proof state after:
case refine_3.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
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) in 𝓝 z, x ∉ t
Theorem: HolomorphicOn.const_of_locally_const
Proof state before:
case refine_3.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
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) in 𝓝 z, x ∉ t
Tactic:
refine h.mp (eventually_of_forall ?_)
Proof state after:
case refine_3.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
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), (x ≠ z → f x ≠ a) → x ∉ t
Theorem: HolomorphicOn.const_of_locally_const
Proof state before:
case refine_3.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
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), (x ≠ z → f x ≠ a) → x ∉ t
Tactic:
intro x i
Proof state after:
case refine_3.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
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
i : x ≠ z → f x ≠ a
⊢ x ∉ t
Theorem: HolomorphicOn.const_of_locally_const
Proof state before:
case refine_3.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
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
i : x ≠ z → f x ≠ a
⊢ x ∉ t
Tactic:
by_cases xz : x = z
Proof state after:
case pos
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
i : x ≠ z → f x ≠ a
xz : x = z
⊢ x ∉ t

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
i : x ≠ z → f x ≠ a
xz : ¬x = z
⊢ x ∉ t
Theorem: HolomorphicOn.const_of_locally_const
Proof state before:
case pos
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
i : x ≠ z → f x ≠ a
xz : x = z
⊢ x ∉ t

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
i : x ≠ z → f x ≠ a
xz : ¬x = z
⊢ x ∉ t
Tactic:
rwa [xz]
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
i : x ≠ z → f x ≠ a
xz : ¬x = z
⊢ x ∉ t
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
i : x ≠ z → f x ≠ a
xz : ¬x = z
⊢ x ∉ t
Tactic:
specialize i xz
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 : f x ≠ a
⊢ x ∉ t
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 : f x ≠ a
⊢ x ∉ t
Tactic:
contrapose 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 ∉ t
⊢ ¬f x ≠ a