internlm/Lean-Github huggingface dataset:
Theorem: NontrivialAnalyticOn.isolated'
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 ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
a : ℂ
h : f z = a
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ a

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 ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
a : ℂ
h : ¬f z = a
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ a
Tactic:
simp only [← h]
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 ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
a : ℂ
h : f z = a
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ f z

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 ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
a : ℂ
h : ¬f z = a
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ a
Theorem: NontrivialAnalyticOn.isolated'
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 ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
a : ℂ
h : f z = a
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ f z

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 ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
a : ℂ
h : ¬f z = a
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ a
Tactic:
exact n.isolated zs
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 ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
a : ℂ
h : ¬f z = a
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ a
Theorem: NontrivialAnalyticOn.isolated'
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 ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
a : ℂ
h : ¬f z = a
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ a
Tactic:
exact ((n.analyticOn _ zs).continuousAt.eventually_ne h).filter_mono nhdsWithin_le_nhds
Proof state after:
no goals
Theorem: IsPreconnected.nontrivialAnalyticOn
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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
ne : ∃ a b, a ∈ s ∧ b ∈ s ∧ f a ≠ f b
⊢ ∀ x ∈ s, ∃ᶠ (y : ℂ) in 𝓝 x, f y ≠ f x
Tactic:
contrapose ne
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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
ne : ¬∀ x ∈ s, ∃ᶠ (y : ℂ) in 𝓝 x, f y ≠ f x
⊢ ¬∃ a b, a ∈ s ∧ b ∈ s ∧ f a ≠ f b
Theorem: IsPreconnected.nontrivialAnalyticOn
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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
ne : ¬∀ x ∈ s, ∃ᶠ (y : ℂ) in 𝓝 x, f y ≠ f x
⊢ ¬∃ a b, a ∈ s ∧ b ∈ s ∧ f a ≠ f b
Tactic:
simp only [not_forall, Filter.not_frequently, not_not] at ne
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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
ne : ∃ x, ∃ (_ : x ∈ s), ∀ᶠ (x_1 : ℂ) in 𝓝 x, f x_1 = f x
⊢ ¬∃ a b, a ∈ s ∧ b ∈ s ∧ f a ≠ f b
Theorem: IsPreconnected.nontrivialAnalyticOn
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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
ne : ∃ x, ∃ (_ : x ∈ s), ∀ᶠ (x_1 : ℂ) in 𝓝 x, f x_1 = f x
⊢ ¬∃ a b, a ∈ s ∧ b ∈ s ∧ f a ≠ f b
Tactic:
rcases ne with ⟨z, zs, h⟩
Proof state after:
case 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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
z : ℂ
zs : z ∈ s
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
⊢ ¬∃ a b, a ∈ s ∧ b ∈ s ∧ f a ≠ f b
Theorem: IsPreconnected.nontrivialAnalyticOn
Proof state before:
case 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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
z : ℂ
zs : z ∈ s
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
⊢ ¬∃ a b, a ∈ s ∧ b ∈ s ∧ f a ≠ f b
Tactic:
simp only [not_exists, exists_and_left, not_and, not_not]
Proof state after:
case 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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
z : ℂ
zs : z ∈ s
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
⊢ ∀ x ∈ s, ∀ x_1 ∈ s, f x = f x_1
Theorem: IsPreconnected.nontrivialAnalyticOn
Proof state before:
case 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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
z : ℂ
zs : z ∈ s
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
⊢ ∀ x ∈ s, ∀ x_1 ∈ s, f x = f x_1
Tactic:
have h' := (h.filter_mono (nhdsWithin_le_nhds (s := {z}ᶜ))).frequently
Proof state after:
case 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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
z : ℂ
zs : z ∈ s
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
h' : ∃ᶠ (x : ℂ) in 𝓝[≠] z, f x = f z
⊢ ∀ x ∈ s, ∀ x_1 ∈ s, f x = f x_1
Theorem: IsPreconnected.nontrivialAnalyticOn
Proof state before:
case 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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
z : ℂ
zs : z ∈ s
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
h' : ∃ᶠ (x : ℂ) in 𝓝[≠] z, f x = f z
⊢ ∀ x ∈ s, ∀ x_1 ∈ s, f x = f x_1
Tactic:
have e := fa.eqOn_of_preconnected_of_frequently_eq analyticOn_const p zs h'
Proof state after:
case 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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
z : ℂ
zs : z ∈ s
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
h' : ∃ᶠ (x : ℂ) in 𝓝[≠] z, f x = f z
e : EqOn f (fun x => f z) s
⊢ ∀ x ∈ s, ∀ x_1 ∈ s, f x = f x_1
Theorem: IsPreconnected.nontrivialAnalyticOn
Proof state before:
case 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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
z : ℂ
zs : z ∈ s
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
h' : ∃ᶠ (x : ℂ) in 𝓝[≠] z, f x = f z
e : EqOn f (fun x => f z) s
⊢ ∀ x ∈ s, ∀ x_1 ∈ s, f x = f x_1
Tactic:
intro x xs y ys
Proof state after:
case 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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
z : ℂ
zs : z ∈ s
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
h' : ∃ᶠ (x : ℂ) in 𝓝[≠] z, f x = f z
e : EqOn f (fun x => f z) s
x : ℂ
xs : x ∈ s
y : ℂ
ys : y ∈ s
⊢ f x = f y
Theorem: IsPreconnected.nontrivialAnalyticOn
Proof state before:
case 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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
z : ℂ
zs : z ∈ s
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
h' : ∃ᶠ (x : ℂ) in 𝓝[≠] z, f x = f z
e : EqOn f (fun x => f z) s
x : ℂ
xs : x ∈ s
y : ℂ
ys : y ∈ s
⊢ f x = f y
Tactic:
rw [e xs, e ys]
Proof state after:
no goals
Theorem: Entire.nontrivialAnalyticOn
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 ℂ
fa : AnalyticOn ℂ f univ
ne : ∃ a b, f a ≠ f b
⊢ NontrivialAnalyticOn f univ
Tactic:
refine isPreconnected_univ.nontrivialAnalyticOn fa ?_
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 ℂ
fa : AnalyticOn ℂ f univ
ne : ∃ a b, f a ≠ f b
⊢ ∃ a b, a ∈ univ ∧ b ∈ univ ∧ f a ≠ f b
Theorem: Entire.nontrivialAnalyticOn
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 ℂ
fa : AnalyticOn ℂ f univ
ne : ∃ a b, f a ≠ f b
⊢ ∃ a b, a ∈ univ ∧ b ∈ univ ∧ f a ≠ f b
Tactic:
simpa only [Set.mem_univ, true_and_iff]
Proof state after:
no goals
Theorem: NontrivialAnalyticOn.discreteTopology
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 ℂ
n : NontrivialAnalyticOn f s
a : ℂ
⊢ DiscreteTopology ↑(s ∩ f ⁻¹' {a})
Tactic:
rw [← singletons_open_iff_discrete]
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 ℂ
n : NontrivialAnalyticOn f s
a : ℂ
⊢ ∀ (a_1 : ↑(s ∩ f ⁻¹' {a})), IsOpen {a_1}
Theorem: NontrivialAnalyticOn.discreteTopology
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 ℂ
n : NontrivialAnalyticOn f s
a : ℂ
⊢ ∀ (a_1 : ↑(s ∩ f ⁻¹' {a})), IsOpen {a_1}
Tactic:
intro ⟨z, m⟩
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 ℂ
n : NontrivialAnalyticOn f s
a z : ℂ
m : z ∈ s ∩ f ⁻¹' {a}
⊢ IsOpen {⟨z, m⟩}
Theorem: NontrivialAnalyticOn.discreteTopology
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 ℂ
n : NontrivialAnalyticOn f s
a z : ℂ
m : z ∈ s ∩ f ⁻¹' {a}
⊢ IsOpen {⟨z, m⟩}
Tactic:
simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_singleton_iff] at m
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 ℂ
n : NontrivialAnalyticOn f s
a z : ℂ
m✝ : z ∈ s ∩ f ⁻¹' {a}
m : z ∈ s ∧ f z = a
⊢ IsOpen {⟨z, m✝⟩}
Theorem: NontrivialAnalyticOn.discreteTopology
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 ℂ
n : NontrivialAnalyticOn f s
a z : ℂ
m✝ : z ∈ s ∩ f ⁻¹' {a}
m : z ∈ s ∧ f z = a
⊢ IsOpen {⟨z, m✝⟩}
Tactic:
by_cases h : ∃ᶠ z in 𝓝[{z}ᶜ] z, f z = a
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 ℂ
n : NontrivialAnalyticOn f s
a z : ℂ
m✝ : z ∈ s ∩ f ⁻¹' {a}
m : z ∈ s ∧ f z = a
h : ∃ᶠ (z : ℂ) in 𝓝[≠] z, f z = a
⊢ IsOpen {⟨z, m✝⟩}

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 ℂ
n : NontrivialAnalyticOn f s
a z : ℂ
m✝ : z ∈ s ∩ f ⁻¹' {a}
m : z ∈ s ∧ f z = a
h : ¬∃ᶠ (z : ℂ) in 𝓝[≠] z, f z = a
⊢ IsOpen {⟨z, m✝⟩}
Theorem: NontrivialAnalyticOn.discreteTopology
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 ℂ
n : NontrivialAnalyticOn f s
a z : ℂ
m✝ : z ∈ s ∩ f ⁻¹' {a}
m : z ∈ s ∧ f z = a
h : ∃ᶠ (z : ℂ) in 𝓝[≠] z, f z = a
⊢ IsOpen {⟨z, m✝⟩}
Tactic:
have i := (n.isolated' m.1 a).and_frequently h
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 ℂ
n : NontrivialAnalyticOn f s
a z : ℂ
m✝ : z ∈ s ∩ f ⁻¹' {a}
m : z ∈ s ∧ f z = a
h : ∃ᶠ (z : ℂ) in 𝓝[≠] z, f z = a
i : ∃ᶠ (x : ℂ) in 𝓝[≠] z, f x ≠ a ∧ f x = a
⊢ IsOpen {⟨z, m✝⟩}
Theorem: NontrivialAnalyticOn.discreteTopology
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 ℂ
n : NontrivialAnalyticOn f s
a z : ℂ
m✝ : z ∈ s ∩ f ⁻¹' {a}
m : z ∈ s ∧ f z = a
h : ∃ᶠ (z : ℂ) in 𝓝[≠] z, f z = a
i : ∃ᶠ (x : ℂ) in 𝓝[≠] z, f x ≠ a ∧ f x = a
⊢ IsOpen {⟨z, m✝⟩}
Tactic:
simp only [not_and_self_iff, Filter.frequently_const] at i
Proof state after:
no goals
Theorem: NontrivialAnalyticOn.discreteTopology
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 ℂ
n : NontrivialAnalyticOn f s
a z : ℂ
m✝ : z ∈ s ∩ f ⁻¹' {a}
m : z ∈ s ∧ f z = a
h : ¬∃ᶠ (z : ℂ) in 𝓝[≠] z, f z = a
⊢ IsOpen {⟨z, m✝⟩}
Tactic:
simp only [Filter.not_frequently, eventually_nhdsWithin_iff, Set.mem_compl_singleton_iff] at h
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 ℂ
n : NontrivialAnalyticOn f s
a z : ℂ
m✝ : z ∈ s ∩ f ⁻¹' {a}
m : z ∈ s ∧ f z = a
h : ∀ᶠ (x : ℂ) in 𝓝 z, x ≠ z → ¬f x = a
⊢ IsOpen {⟨z, m✝⟩}
Theorem: NontrivialAnalyticOn.discreteTopology
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 ℂ
n : NontrivialAnalyticOn f s
a z : ℂ
m✝ : z ∈ s ∩ f ⁻¹' {a}
m : z ∈ s ∧ f z = a
h : ∀ᶠ (x : ℂ) in 𝓝 z, x ≠ z → ¬f x = a
⊢ IsOpen {⟨z, m✝⟩}
Tactic:
rcases eventually_nhds_iff.mp h with ⟨t, t0, o, tz⟩
Proof state after:
case neg.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 ℂ
n : NontrivialAnalyticOn f s
a z : ℂ
m✝ : z ∈ s ∩ f ⁻¹' {a}
m : z ∈ s ∧ f z = a
h : ∀ᶠ (x : ℂ) in 𝓝 z, x ≠ z → ¬f x = a
t : Set ℂ
t0 : ∀ x ∈ t, x ≠ z → ¬f x = a
o : IsOpen t
tz : z ∈ t
⊢ IsOpen {⟨z, m✝⟩}
Theorem: NontrivialAnalyticOn.discreteTopology
Proof state before:
case neg.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 ℂ
n : NontrivialAnalyticOn f s
a z : ℂ
m✝ : z ∈ s ∩ f ⁻¹' {a}
m : z ∈ s ∧ f z = a
h : ∀ᶠ (x : ℂ) in 𝓝 z, x ≠ z → ¬f x = a
t : Set ℂ
t0 : ∀ x ∈ t, x ≠ z → ¬f x = a
o : IsOpen t
tz : z ∈ t
⊢ IsOpen {⟨z, m✝⟩}
Tactic:
simp only [isOpen_induced_iff]
Proof state after:
case neg.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 ℂ
n : NontrivialAnalyticOn f s
a z : ℂ
m✝ : z ∈ s ∩ f ⁻¹' {a}
m : z ∈ s ∧ f z = a
h : ∀ᶠ (x : ℂ) in 𝓝 z, x ≠ z → ¬f x = a
t : Set ℂ
t0 : ∀ x ∈ t, x ≠ z → ¬f x = a
o : IsOpen t
tz : z ∈ t
⊢ ∃ t, IsOpen t ∧ Subtype.val ⁻¹' t = {⟨z, m✝⟩}