internlm/Lean-Github huggingface dataset:
Theorem: nontrivialHolomorphicAt_of_order
Proof 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✝ : ℂ → ℂ
s : Set ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
fp : HasFPowerSeriesAt f (constFormalMultilinearSeries ℂ ℂ (f z)) z
p0 : ¬(constFormalMultilinearSeries ℂ ℂ (f z)).order = 0
b : constFormalMultilinearSeries ℂ ℂ (f z) (constFormalMultilinearSeries ℂ ℂ (f z)).order ≠ 0
⊢ False
Tactic:
simp only [constFormalMultilinearSeries_apply p0, Ne, eq_self_iff_true, not_true] at b
Proof state after:
no goals
Theorem: NontrivialHolomorphicAt.pow_iff
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 ℂ
f : S → ℂ
z : S
d : ℕ
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d0 : 0 < d
⊢ NontrivialHolomorphicAt (fun z => f z ^ d) z ↔ NontrivialHolomorphicAt f z
Tactic:
refine ⟨?_, (nontrivialHolomorphicAtPow d0).comp⟩
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 ℂ
f : S → ℂ
z : S
d : ℕ
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d0 : 0 < d
⊢ NontrivialHolomorphicAt (fun z => f z ^ d) z → NontrivialHolomorphicAt f z
Theorem: NontrivialHolomorphicAt.pow_iff
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 ℂ
f : S → ℂ
z : S
d : ℕ
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d0 : 0 < d
⊢ NontrivialHolomorphicAt (fun z => f z ^ d) z → NontrivialHolomorphicAt f z
Tactic:
have pa : HolomorphicAt I I (fun z ↦ z ^ d) (f z) := HolomorphicAt.pow holomorphicAt_id
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 ℂ
f : S → ℂ
z : S
d : ℕ
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d0 : 0 < d
pa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun z => z ^ d) (f z)
⊢ NontrivialHolomorphicAt (fun z => f z ^ d) z → NontrivialHolomorphicAt f z
Theorem: NontrivialHolomorphicAt.pow_iff
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 ℂ
f : S → ℂ
z : S
d : ℕ
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d0 : 0 < d
pa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun z => z ^ d) (f z)
⊢ NontrivialHolomorphicAt (fun z => f z ^ d) z → NontrivialHolomorphicAt f z
Tactic:
intro h
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 ℂ
f : S → ℂ
z : S
d : ℕ
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d0 : 0 < d
pa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun z => z ^ d) (f z)
h : NontrivialHolomorphicAt (fun z => f z ^ d) z
⊢ NontrivialHolomorphicAt f z
Theorem: NontrivialHolomorphicAt.pow_iff
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 ℂ
f : S → ℂ
z : S
d : ℕ
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d0 : 0 < d
pa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun z => z ^ d) (f z)
h : NontrivialHolomorphicAt (fun z => f z ^ d) z
⊢ NontrivialHolomorphicAt f z
Tactic:
refine (NontrivialHolomorphicAt.anti ?_ pa fa).2
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 ℂ
f : S → ℂ
z : S
d : ℕ
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d0 : 0 < d
pa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun z => z ^ d) (f z)
h : NontrivialHolomorphicAt (fun z => f z ^ d) z
⊢ NontrivialHolomorphicAt (fun z => f z ^ d) z
Theorem: NontrivialHolomorphicAt.pow_iff
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 ℂ
f : S → ℂ
z : S
d : ℕ
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d0 : 0 < d
pa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun z => z ^ d) (f z)
h : NontrivialHolomorphicAt (fun z => f z ^ d) z
⊢ NontrivialHolomorphicAt (fun z => f z ^ d) z
Tactic:
exact h
Proof state after:
no goals
Theorem: NontrivialHolomorphicAt.congr
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 ℂ
f g : S → T
z : S
n : NontrivialHolomorphicAt f z
e : (𝓝 z).EventuallyEq f g
⊢ NontrivialHolomorphicAt g z
Tactic:
use n.holomorphicAt.congr e
Proof 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✝ : ℂ → ℂ
s : Set ℂ
f g : S → T
z : S
n : NontrivialHolomorphicAt f z
e : (𝓝 z).EventuallyEq f g
⊢ ∃ᶠ (w : S) in 𝓝 z, g w ≠ g z
Theorem: NontrivialHolomorphicAt.congr
Proof 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✝ : ℂ → ℂ
s : Set ℂ
f g : S → T
z : S
n : NontrivialHolomorphicAt f z
e : (𝓝 z).EventuallyEq f g
⊢ ∃ᶠ (w : S) in 𝓝 z, g w ≠ g z
Tactic:
refine n.nonconst.mp (e.mp (eventually_of_forall fun w ew n ↦ ?_))
Proof 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✝ : ℂ → ℂ
s : Set ℂ
f g : S → T
z : S
n✝ : NontrivialHolomorphicAt f z
e : (𝓝 z).EventuallyEq f g
w : S
ew : f w = g w
n : f w ≠ f z
⊢ g w ≠ g z
Theorem: NontrivialHolomorphicAt.congr
Proof 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✝ : ℂ → ℂ
s : Set ℂ
f g : S → T
z : S
n✝ : NontrivialHolomorphicAt f z
e : (𝓝 z).EventuallyEq f g
w : S
ew : f w = g w
n : f w ≠ f z
⊢ g w ≠ g z
Tactic:
rwa [← ew, ← e.self_of_nhds]
Proof state after:
no goals
Theorem: HolomorphicOn.eq_of_locally_eq
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 ℂ
E : Type
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace ℂ E
inst✝¹⁴ : CompleteSpace E
F : Type
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace ℂ F
inst✝¹¹ : CompleteSpace F
A : Type
inst✝¹⁰ : TopologicalSpace A
J : ModelWithCorners ℂ E A
inst✝⁹ : J.Boundaryless
B : Type
inst✝⁸ : TopologicalSpace B
K : ModelWithCorners ℂ F B
inst✝⁷ : K.Boundaryless
M : Type
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace A M
inst✝⁴ : AnalyticManifold J M
N : Type
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace B N
inst✝¹ : AnalyticManifold K N
f g : M → N
inst✝ : T2Space N
s : Set M
fa : HolomorphicOn J K f s
ga : HolomorphicOn J K g s
sp : IsPreconnected s
e : ∃ x ∈ s, (𝓝 x).EventuallyEq f g
⊢ (𝓝ˢ s).EventuallyEq f g
Tactic:
generalize ht :  {x | f =ᶠ[𝓝 x] g} = 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 ℂ
E : Type
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace ℂ E
inst✝¹⁴ : CompleteSpace E
F : Type
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace ℂ F
inst✝¹¹ : CompleteSpace F
A : Type
inst✝¹⁰ : TopologicalSpace A
J : ModelWithCorners ℂ E A
inst✝⁹ : J.Boundaryless
B : Type
inst✝⁸ : TopologicalSpace B
K : ModelWithCorners ℂ F B
inst✝⁷ : K.Boundaryless
M : Type
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace A M
inst✝⁴ : AnalyticManifold J M
N : Type
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace B N
inst✝¹ : AnalyticManifold K N
f g : M → N
inst✝ : T2Space N
s : Set M
fa : HolomorphicOn J K f s
ga : HolomorphicOn J K g s
sp : IsPreconnected s
e : ∃ x ∈ s, (𝓝 x).EventuallyEq f g
t : Set M
ht : {x | (𝓝 x).EventuallyEq f g} = t
⊢ (𝓝ˢ s).EventuallyEq f g
Theorem: HolomorphicOn.eq_of_locally_eq
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 ℂ
E : Type
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace ℂ E
inst✝¹⁴ : CompleteSpace E
F : Type
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace ℂ F
inst✝¹¹ : CompleteSpace F
A : Type
inst✝¹⁰ : TopologicalSpace A
J : ModelWithCorners ℂ E A
inst✝⁹ : J.Boundaryless
B : Type
inst✝⁸ : TopologicalSpace B
K : ModelWithCorners ℂ F B
inst✝⁷ : K.Boundaryless
M : Type
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace A M
inst✝⁴ : AnalyticManifold J M
N : Type
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace B N
inst✝¹ : AnalyticManifold K N
f g : M → N
inst✝ : T2Space N
s : Set M
fa : HolomorphicOn J K f s
ga : HolomorphicOn J K g s
sp : IsPreconnected s
e : ∃ x ∈ s, (𝓝 x).EventuallyEq f g
t : Set M
ht : {x | (𝓝 x).EventuallyEq f g} = t
⊢ (𝓝ˢ s).EventuallyEq f g
Tactic:
suffices h : s ⊆ interior t by
  simp only [subset_interior_iff_mem_nhdsSet, ← Filter.eventually_iff, ← ht] at h
  exact h.mp (eventually_of_forall fun _ e ↦ e.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 ℂ
E : Type
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace ℂ E
inst✝¹⁴ : CompleteSpace E
F : Type
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace ℂ F
inst✝¹¹ : CompleteSpace F
A : Type
inst✝¹⁰ : TopologicalSpace A
J : ModelWithCorners ℂ E A
inst✝⁹ : J.Boundaryless
B : Type
inst✝⁸ : TopologicalSpace B
K : ModelWithCorners ℂ F B
inst✝⁷ : K.Boundaryless
M : Type
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace A M
inst✝⁴ : AnalyticManifold J M
N : Type
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace B N
inst✝¹ : AnalyticManifold K N
f g : M → N
inst✝ : T2Space N
s : Set M
fa : HolomorphicOn J K f s
ga : HolomorphicOn J K g s
sp : IsPreconnected s
e : ∃ x ∈ s, (𝓝 x).EventuallyEq f g
t : Set M
ht : {x | (𝓝 x).EventuallyEq f g} = t
⊢ s ⊆ interior t
Theorem: HolomorphicOn.eq_of_locally_eq
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 ℂ
E : Type
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace ℂ E
inst✝¹⁴ : CompleteSpace E
F : Type
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace ℂ F
inst✝¹¹ : CompleteSpace F
A : Type
inst✝¹⁰ : TopologicalSpace A
J : ModelWithCorners ℂ E A
inst✝⁹ : J.Boundaryless
B : Type
inst✝⁸ : TopologicalSpace B
K : ModelWithCorners ℂ F B
inst✝⁷ : K.Boundaryless
M : Type
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace A M
inst✝⁴ : AnalyticManifold J M
N : Type
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace B N
inst✝¹ : AnalyticManifold K N
f g : M → N
inst✝ : T2Space N
s : Set M
fa : HolomorphicOn J K f s
ga : HolomorphicOn J K g s
sp : IsPreconnected s
e : ∃ x ∈ s, (𝓝 x).EventuallyEq f g
t : Set M
ht : {x | (𝓝 x).EventuallyEq f g} = t
h : s ⊆ interior t
⊢ (𝓝ˢ s).EventuallyEq f g
Tactic:
simp only [subset_interior_iff_mem_nhdsSet, ← Filter.eventually_iff, ← ht] at h
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 ℂ
E : Type
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace ℂ E
inst✝¹⁴ : CompleteSpace E
F : Type
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace ℂ F
inst✝¹¹ : CompleteSpace F
A : Type
inst✝¹⁰ : TopologicalSpace A
J : ModelWithCorners ℂ E A
inst✝⁹ : J.Boundaryless
B : Type
inst✝⁸ : TopologicalSpace B
K : ModelWithCorners ℂ F B
inst✝⁷ : K.Boundaryless
M : Type
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace A M
inst✝⁴ : AnalyticManifold J M
N : Type
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace B N
inst✝¹ : AnalyticManifold K N
f g : M → N
inst✝ : T2Space N
s : Set M
fa : HolomorphicOn J K f s
ga : HolomorphicOn J K g s
sp : IsPreconnected s
e : ∃ x ∈ s, (𝓝 x).EventuallyEq f g
t : Set M
ht : {x | (𝓝 x).EventuallyEq f g} = t
h : ∀ᶠ (x : M) in 𝓝ˢ s, (𝓝 x).EventuallyEq f g
⊢ (𝓝ˢ s).EventuallyEq f g
Theorem: HolomorphicOn.eq_of_locally_eq
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 ℂ
E : Type
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace ℂ E
inst✝¹⁴ : CompleteSpace E
F : Type
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace ℂ F
inst✝¹¹ : CompleteSpace F
A : Type
inst✝¹⁰ : TopologicalSpace A
J : ModelWithCorners ℂ E A
inst✝⁹ : J.Boundaryless
B : Type
inst✝⁸ : TopologicalSpace B
K : ModelWithCorners ℂ F B
inst✝⁷ : K.Boundaryless
M : Type
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace A M
inst✝⁴ : AnalyticManifold J M
N : Type
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace B N
inst✝¹ : AnalyticManifold K N
f g : M → N
inst✝ : T2Space N
s : Set M
fa : HolomorphicOn J K f s
ga : HolomorphicOn J K g s
sp : IsPreconnected s
e : ∃ x ∈ s, (𝓝 x).EventuallyEq f g
t : Set M
ht : {x | (𝓝 x).EventuallyEq f g} = t
h : ∀ᶠ (x : M) in 𝓝ˢ s, (𝓝 x).EventuallyEq f g
⊢ (𝓝ˢ s).EventuallyEq f g
Tactic:
exact h.mp (eventually_of_forall fun _ e ↦ e.self_of_nhds)
Proof state after:
no goals
Theorem: HolomorphicOn.eq_of_locally_eq
Proof state before:
case ne
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 ℂ
E : Type
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace ℂ E
inst✝¹⁴ : CompleteSpace E
F : Type
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace ℂ F
inst✝¹¹ : CompleteSpace F
A : Type
inst✝¹⁰ : TopologicalSpace A
J : ModelWithCorners ℂ E A
inst✝⁹ : J.Boundaryless
B : Type
inst✝⁸ : TopologicalSpace B
K : ModelWithCorners ℂ F B
inst✝⁷ : K.Boundaryless
M : Type
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace A M
inst✝⁴ : AnalyticManifold J M
N : Type
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace B N
inst✝¹ : AnalyticManifold K N
f g : M → N
inst✝ : T2Space N
s : Set M
fa : HolomorphicOn J K f s
ga : HolomorphicOn J K g s
sp : IsPreconnected s
e : ∃ x ∈ s, (𝓝 x).EventuallyEq f g
t : Set M
ht : {x | (𝓝 x).EventuallyEq f g} = t
⊢ (s ∩ t).Nonempty
Tactic:
rw [← ht]
Proof state after:
case ne
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 ℂ
E : Type
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace ℂ E
inst✝¹⁴ : CompleteSpace E
F : Type
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace ℂ F
inst✝¹¹ : CompleteSpace F
A : Type
inst✝¹⁰ : TopologicalSpace A
J : ModelWithCorners ℂ E A
inst✝⁹ : J.Boundaryless
B : Type
inst✝⁸ : TopologicalSpace B
K : ModelWithCorners ℂ F B
inst✝⁷ : K.Boundaryless
M : Type
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace A M
inst✝⁴ : AnalyticManifold J M
N : Type
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace B N
inst✝¹ : AnalyticManifold K N
f g : M → N
inst✝ : T2Space N
s : Set M
fa : HolomorphicOn J K f s
ga : HolomorphicOn J K g s
sp : IsPreconnected s
e : ∃ x ∈ s, (𝓝 x).EventuallyEq f g
t : Set M
ht : {x | (𝓝 x).EventuallyEq f g} = t
⊢ (s ∩ {x | (𝓝 x).EventuallyEq f g}).Nonempty
Theorem: HolomorphicOn.eq_of_locally_eq
Proof state before:
case ne
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 ℂ
E : Type
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace ℂ E
inst✝¹⁴ : CompleteSpace E
F : Type
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace ℂ F
inst✝¹¹ : CompleteSpace F
A : Type
inst✝¹⁰ : TopologicalSpace A
J : ModelWithCorners ℂ E A
inst✝⁹ : J.Boundaryless
B : Type
inst✝⁸ : TopologicalSpace B
K : ModelWithCorners ℂ F B
inst✝⁷ : K.Boundaryless
M : Type
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace A M
inst✝⁴ : AnalyticManifold J M
N : Type
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace B N
inst✝¹ : AnalyticManifold K N
f g : M → N
inst✝ : T2Space N
s : Set M
fa : HolomorphicOn J K f s
ga : HolomorphicOn J K g s
sp : IsPreconnected s
e : ∃ x ∈ s, (𝓝 x).EventuallyEq f g
t : Set M
ht : {x | (𝓝 x).EventuallyEq f g} = t
⊢ (s ∩ {x | (𝓝 x).EventuallyEq f g}).Nonempty
Tactic:
exact e
Proof state after:
no goals
Theorem: HolomorphicOn.eq_of_locally_eq
Proof state before:
case op
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 ℂ
E : Type
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace ℂ E
inst✝¹⁴ : CompleteSpace E
F : Type
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace ℂ F
inst✝¹¹ : CompleteSpace F
A : Type
inst✝¹⁰ : TopologicalSpace A
J : ModelWithCorners ℂ E A
inst✝⁹ : J.Boundaryless
B : Type
inst✝⁸ : TopologicalSpace B
K : ModelWithCorners ℂ F B
inst✝⁷ : K.Boundaryless
M : Type
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace A M
inst✝⁴ : AnalyticManifold J M
N : Type
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace B N
inst✝¹ : AnalyticManifold K N
f g : M → N
inst✝ : T2Space N
s : Set M
fa : HolomorphicOn J K f s
ga : HolomorphicOn J K g s
sp : IsPreconnected s
e : ∃ x ∈ s, (𝓝 x).EventuallyEq f g
t : Set M
ht : {x | (𝓝 x).EventuallyEq f g} = t
⊢ s ∩ t ⊆ interior t
Tactic:
intro x ⟨_, xt⟩
Proof state after:
case op
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 ℂ
E : Type
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace ℂ E
inst✝¹⁴ : CompleteSpace E
F : Type
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace ℂ F
inst✝¹¹ : CompleteSpace F
A : Type
inst✝¹⁰ : TopologicalSpace A
J : ModelWithCorners ℂ E A
inst✝⁹ : J.Boundaryless
B : Type
inst✝⁸ : TopologicalSpace B
K : ModelWithCorners ℂ F B
inst✝⁷ : K.Boundaryless
M : Type
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace A M
inst✝⁴ : AnalyticManifold J M
N : Type
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace B N
inst✝¹ : AnalyticManifold K N
f g : M → N
inst✝ : T2Space N
s : Set M
fa : HolomorphicOn J K f s
ga : HolomorphicOn J K g s
sp : IsPreconnected s
e : ∃ x ∈ s, (𝓝 x).EventuallyEq f g
t : Set M
ht : {x | (𝓝 x).EventuallyEq f g} = t
x : M
left✝ : x ∈ s
xt : x ∈ t
⊢ x ∈ interior t