internlm/Lean-Github huggingface dataset:
Theorem: IsPreconnected.open_diff
Proof state before:
case intro.intro.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
f : Set X → Set X
hf : (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) = f
mono : ∀ (u : Set X), u ⊆ f u
fopen : ∀ {u : Set X}, IsOpen u → IsOpen (f u)
mem : ∀ {x : X} {u c : Set X}, x ∈ s → x ∈ t → c ∈ 𝓝[tᶜ] x → c ⊆ u → x ∈ f u
cover : s ⊆ f u ∪ f v
fdiff : ∀ {u : Set X}, f u \ t ⊆ u
fnon : ∀ {x : X} {u : Set X}, IsOpen u → x ∈ f u → ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u
x : X
m : x ∈ s ∧ x ∈ f u ∧ x ∈ f v
b : ∀ᶠ (x : X) in 𝓝 x, x ∈ tᶜ → x ∈ s ∧ x ∈ u ∧ x ∈ v
n : Set X
h : ∀ x ∈ n, x ∈ tᶜ → x ∈ s ∧ x ∈ u ∧ x ∈ v
no : IsOpen n
xn : x ∈ n
⊢ (s \ t ∩ (u ∩ v)).Nonempty
Tactic:
rcases ts.dense.exists_mem_open no ⟨_, xn⟩ with ⟨y, yt, yn⟩
Proof state after:
case intro.intro.intro.intro.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
f : Set X → Set X
hf : (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) = f
mono : ∀ (u : Set X), u ⊆ f u
fopen : ∀ {u : Set X}, IsOpen u → IsOpen (f u)
mem : ∀ {x : X} {u c : Set X}, x ∈ s → x ∈ t → c ∈ 𝓝[tᶜ] x → c ⊆ u → x ∈ f u
cover : s ⊆ f u ∪ f v
fdiff : ∀ {u : Set X}, f u \ t ⊆ u
fnon : ∀ {x : X} {u : Set X}, IsOpen u → x ∈ f u → ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u
x : X
m : x ∈ s ∧ x ∈ f u ∧ x ∈ f v
b : ∀ᶠ (x : X) in 𝓝 x, x ∈ tᶜ → x ∈ s ∧ x ∈ u ∧ x ∈ v
n : Set X
h : ∀ x ∈ n, x ∈ tᶜ → x ∈ s ∧ x ∈ u ∧ x ∈ v
no : IsOpen n
xn : x ∈ n
y : X
yt : y ∈ tᶜ
yn : y ∈ n
⊢ (s \ t ∩ (u ∩ v)).Nonempty
Theorem: IsPreconnected.open_diff
Proof state before:
case intro.intro.intro.intro.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
f : Set X → Set X
hf : (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) = f
mono : ∀ (u : Set X), u ⊆ f u
fopen : ∀ {u : Set X}, IsOpen u → IsOpen (f u)
mem : ∀ {x : X} {u c : Set X}, x ∈ s → x ∈ t → c ∈ 𝓝[tᶜ] x → c ⊆ u → x ∈ f u
cover : s ⊆ f u ∪ f v
fdiff : ∀ {u : Set X}, f u \ t ⊆ u
fnon : ∀ {x : X} {u : Set X}, IsOpen u → x ∈ f u → ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u
x : X
m : x ∈ s ∧ x ∈ f u ∧ x ∈ f v
b : ∀ᶠ (x : X) in 𝓝 x, x ∈ tᶜ → x ∈ s ∧ x ∈ u ∧ x ∈ v
n : Set X
h : ∀ x ∈ n, x ∈ tᶜ → x ∈ s ∧ x ∈ u ∧ x ∈ v
no : IsOpen n
xn : x ∈ n
y : X
yt : y ∈ tᶜ
yn : y ∈ n
⊢ (s \ t ∩ (u ∩ v)).Nonempty
Tactic:
use y
Proof state after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
f : Set X → Set X
hf : (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) = f
mono : ∀ (u : Set X), u ⊆ f u
fopen : ∀ {u : Set X}, IsOpen u → IsOpen (f u)
mem : ∀ {x : X} {u c : Set X}, x ∈ s → x ∈ t → c ∈ 𝓝[tᶜ] x → c ⊆ u → x ∈ f u
cover : s ⊆ f u ∪ f v
fdiff : ∀ {u : Set X}, f u \ t ⊆ u
fnon : ∀ {x : X} {u : Set X}, IsOpen u → x ∈ f u → ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u
x : X
m : x ∈ s ∧ x ∈ f u ∧ x ∈ f v
b : ∀ᶠ (x : X) in 𝓝 x, x ∈ tᶜ → x ∈ s ∧ x ∈ u ∧ x ∈ v
n : Set X
h : ∀ x ∈ n, x ∈ tᶜ → x ∈ s ∧ x ∈ u ∧ x ∈ v
no : IsOpen n
xn : x ∈ n
y : X
yt : y ∈ tᶜ
yn : y ∈ n
⊢ y ∈ s \ t ∩ (u ∩ v)
Theorem: IsPreconnected.open_diff
Proof state before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
f : Set X → Set X
hf : (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) = f
mono : ∀ (u : Set X), u ⊆ f u
fopen : ∀ {u : Set X}, IsOpen u → IsOpen (f u)
mem : ∀ {x : X} {u c : Set X}, x ∈ s → x ∈ t → c ∈ 𝓝[tᶜ] x → c ⊆ u → x ∈ f u
cover : s ⊆ f u ∪ f v
fdiff : ∀ {u : Set X}, f u \ t ⊆ u
fnon : ∀ {x : X} {u : Set X}, IsOpen u → x ∈ f u → ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u
x : X
m : x ∈ s ∧ x ∈ f u ∧ x ∈ f v
b : ∀ᶠ (x : X) in 𝓝 x, x ∈ tᶜ → x ∈ s ∧ x ∈ u ∧ x ∈ v
n : Set X
h : ∀ x ∈ n, x ∈ tᶜ → x ∈ s ∧ x ∈ u ∧ x ∈ v
no : IsOpen n
xn : x ∈ n
y : X
yt : y ∈ tᶜ
yn : y ∈ n
⊢ y ∈ s \ t ∩ (u ∩ v)
Tactic:
simp only [mem_inter_iff, mem_diff, ← mem_compl_iff]
Proof state after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
f : Set X → Set X
hf : (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) = f
mono : ∀ (u : Set X), u ⊆ f u
fopen : ∀ {u : Set X}, IsOpen u → IsOpen (f u)
mem : ∀ {x : X} {u c : Set X}, x ∈ s → x ∈ t → c ∈ 𝓝[tᶜ] x → c ⊆ u → x ∈ f u
cover : s ⊆ f u ∪ f v
fdiff : ∀ {u : Set X}, f u \ t ⊆ u
fnon : ∀ {x : X} {u : Set X}, IsOpen u → x ∈ f u → ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u
x : X
m : x ∈ s ∧ x ∈ f u ∧ x ∈ f v
b : ∀ᶠ (x : X) in 𝓝 x, x ∈ tᶜ → x ∈ s ∧ x ∈ u ∧ x ∈ v
n : Set X
h : ∀ x ∈ n, x ∈ tᶜ → x ∈ s ∧ x ∈ u ∧ x ∈ v
no : IsOpen n
xn : x ∈ n
y : X
yt : y ∈ tᶜ
yn : y ∈ n
⊢ (y ∈ s ∧ y ∈ tᶜ) ∧ y ∈ u ∧ y ∈ v
Theorem: IsPreconnected.open_diff
Proof state before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
f : Set X → Set X
hf : (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) = f
mono : ∀ (u : Set X), u ⊆ f u
fopen : ∀ {u : Set X}, IsOpen u → IsOpen (f u)
mem : ∀ {x : X} {u c : Set X}, x ∈ s → x ∈ t → c ∈ 𝓝[tᶜ] x → c ⊆ u → x ∈ f u
cover : s ⊆ f u ∪ f v
fdiff : ∀ {u : Set X}, f u \ t ⊆ u
fnon : ∀ {x : X} {u : Set X}, IsOpen u → x ∈ f u → ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u
x : X
m : x ∈ s ∧ x ∈ f u ∧ x ∈ f v
b : ∀ᶠ (x : X) in 𝓝 x, x ∈ tᶜ → x ∈ s ∧ x ∈ u ∧ x ∈ v
n : Set X
h : ∀ x ∈ n, x ∈ tᶜ → x ∈ s ∧ x ∈ u ∧ x ∈ v
no : IsOpen n
xn : x ∈ n
y : X
yt : y ∈ tᶜ
yn : y ∈ n
⊢ (y ∈ s ∧ y ∈ tᶜ) ∧ y ∈ u ∧ y ∈ v
Tactic:
specialize h y yn yt
Proof state after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
f : Set X → Set X
hf : (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) = f
mono : ∀ (u : Set X), u ⊆ f u
fopen : ∀ {u : Set X}, IsOpen u → IsOpen (f u)
mem : ∀ {x : X} {u c : Set X}, x ∈ s → x ∈ t → c ∈ 𝓝[tᶜ] x → c ⊆ u → x ∈ f u
cover : s ⊆ f u ∪ f v
fdiff : ∀ {u : Set X}, f u \ t ⊆ u
fnon : ∀ {x : X} {u : Set X}, IsOpen u → x ∈ f u → ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u
x : X
m : x ∈ s ∧ x ∈ f u ∧ x ∈ f v
b : ∀ᶠ (x : X) in 𝓝 x, x ∈ tᶜ → x ∈ s ∧ x ∈ u ∧ x ∈ v
n : Set X
no : IsOpen n
xn : x ∈ n
y : X
yt : y ∈ tᶜ
yn : y ∈ n
h : y ∈ s ∧ y ∈ u ∧ y ∈ v
⊢ (y ∈ s ∧ y ∈ tᶜ) ∧ y ∈ u ∧ y ∈ v
Theorem: IsPreconnected.open_diff
Proof state before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
f : Set X → Set X
hf : (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) = f
mono : ∀ (u : Set X), u ⊆ f u
fopen : ∀ {u : Set X}, IsOpen u → IsOpen (f u)
mem : ∀ {x : X} {u c : Set X}, x ∈ s → x ∈ t → c ∈ 𝓝[tᶜ] x → c ⊆ u → x ∈ f u
cover : s ⊆ f u ∪ f v
fdiff : ∀ {u : Set X}, f u \ t ⊆ u
fnon : ∀ {x : X} {u : Set X}, IsOpen u → x ∈ f u → ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u
x : X
m : x ∈ s ∧ x ∈ f u ∧ x ∈ f v
b : ∀ᶠ (x : X) in 𝓝 x, x ∈ tᶜ → x ∈ s ∧ x ∈ u ∧ x ∈ v
n : Set X
no : IsOpen n
xn : x ∈ n
y : X
yt : y ∈ tᶜ
yn : y ∈ n
h : y ∈ s ∧ y ∈ u ∧ y ∈ v
⊢ (y ∈ s ∧ y ∈ tᶜ) ∧ y ∈ u ∧ y ∈ v
Tactic:
exact ⟨⟨h.1,yt⟩,h.2.1,h.2.2⟩
Proof state after:
no goals
Theorem: Nonseparating.empty
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
⊢ Dense ∅ᶜ
Tactic:
simp only [compl_empty, dense_univ]
Proof state after:
no goals
Theorem: Nonseparating.empty
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
⊢ ∀ (x : X) (u : Set X), x ∈ ∅ → u ∈ 𝓝 x → ∃ c ⊆ u \ ∅, c ∈ 𝓝[∅ᶜ] x ∧ IsPreconnected c
Tactic:
simp only [mem_empty_iff_false, IsEmpty.forall_iff, forall_const, imp_true_iff]
Proof state after:
no goals
Theorem: IsPreconnected.ball_diff_center
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
⊢ IsPreconnected (ball a r \ {a})
Tactic:
by_cases rp : r ≤ 0
Proof state after:
case pos
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : r ≤ 0
⊢ IsPreconnected (ball a r \ {a})

case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : ¬r ≤ 0
⊢ IsPreconnected (ball a r \ {a})
Theorem: IsPreconnected.ball_diff_center
Proof state before:
case pos
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : r ≤ 0
⊢ IsPreconnected (ball a r \ {a})

case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : ¬r ≤ 0
⊢ IsPreconnected (ball a r \ {a})
Tactic:
simp only [Metric.ball_eq_empty.mpr rp, empty_diff]
Proof state after:
case pos
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : r ≤ 0
⊢ IsPreconnected ∅

case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : ¬r ≤ 0
⊢ IsPreconnected (ball a r \ {a})
Theorem: IsPreconnected.ball_diff_center
Proof state before:
case pos
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : r ≤ 0
⊢ IsPreconnected ∅

case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : ¬r ≤ 0
⊢ IsPreconnected (ball a r \ {a})
Tactic:
exact isPreconnected_empty
Proof state after:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : ¬r ≤ 0
⊢ IsPreconnected (ball a r \ {a})
Theorem: IsPreconnected.ball_diff_center
Proof state before:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : ¬r ≤ 0
⊢ IsPreconnected (ball a r \ {a})
Tactic:
simp only [not_le] at rp
Proof state after:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
⊢ IsPreconnected (ball a r \ {a})
Theorem: IsPreconnected.ball_diff_center
Proof state before:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
e : ball a r \ {a} = (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
⊢ IsPreconnected (ball a r \ {a})
Tactic:
rw [e]
Proof state after:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
e : ball a r \ {a} = (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
⊢ IsPreconnected ((fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ)
Theorem: IsPreconnected.ball_diff_center
Proof state before:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
e : ball a r \ {a} = (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
⊢ IsPreconnected ((fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ)
Tactic:
apply IsPreconnected.image
Proof state after:
case neg.H
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
e : ball a r \ {a} = (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
⊢ IsPreconnected (Ioo 0 r ×ˢ univ)

case neg.hf
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
e : ball a r \ {a} = (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
⊢ ContinuousOn (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) (Ioo 0 r ×ˢ univ)
Theorem: IsPreconnected.ball_diff_center
Proof state before:
case neg.H
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
e : ball a r \ {a} = (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
⊢ IsPreconnected (Ioo 0 r ×ˢ univ)

case neg.hf
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
e : ball a r \ {a} = (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
⊢ ContinuousOn (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) (Ioo 0 r ×ˢ univ)
Tactic:
exact isPreconnected_Ioo.prod isPreconnected_univ
Proof state after:
case neg.hf
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
e : ball a r \ {a} = (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
⊢ ContinuousOn (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) (Ioo 0 r ×ˢ univ)
Theorem: IsPreconnected.ball_diff_center
Proof state before:
case neg.hf
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
e : ball a r \ {a} = (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
⊢ ContinuousOn (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) (Ioo 0 r ×ˢ univ)
Tactic:
apply Continuous.continuousOn
Proof state after:
case neg.hf.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
e : ball a r \ {a} = (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
⊢ Continuous fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp
Theorem: IsPreconnected.ball_diff_center
Proof state before:
case neg.hf.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
e : ball a r \ {a} = (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
⊢ Continuous fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp
Tactic:
continuity
Proof state after:
no goals
Theorem: IsPreconnected.ball_diff_center
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
⊢ ball a r \ {a} = (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
Tactic:
apply Set.ext
Proof state after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
⊢ ∀ (x : ℂ), x ∈ ball a r \ {a} ↔ x ∈ (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
Theorem: IsPreconnected.ball_diff_center
Proof state before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
⊢ ∀ (x : ℂ), x ∈ ball a r \ {a} ↔ x ∈ (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
Tactic:
intro z
Proof state after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
⊢ z ∈ ball a r \ {a} ↔ z ∈ (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
Theorem: IsPreconnected.ball_diff_center
Proof state before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
⊢ z ∈ ball a r \ {a} ↔ z ∈ (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
Tactic:
simp only [mem_diff, mem_ball, Complex.dist_eq, mem_singleton_iff, mem_image, Prod.exists,
  mem_prod_eq, mem_Ioo, mem_univ, and_true_iff]
Proof state after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
⊢ Complex.abs (z - a) < r ∧ ¬z = a ↔ ∃ a_1 b, (0 < a_1 ∧ a_1 < r) ∧ a + ↑a_1 * (↑b * Complex.I).exp = z
Theorem: IsPreconnected.ball_diff_center
Proof state before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
⊢ Complex.abs (z - a) < r ∧ ¬z = a ↔ ∃ a_1 b, (0 < a_1 ∧ a_1 < r) ∧ a + ↑a_1 * (↑b * Complex.I).exp = z
Tactic:
constructor
Proof state after:
case h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
⊢ Complex.abs (z - a) < r ∧ ¬z = a → ∃ a_2 b, (0 < a_2 ∧ a_2 < r) ∧ a + ↑a_2 * (↑b * Complex.I).exp = z

case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
⊢ (∃ a_1 b, (0 < a_1 ∧ a_1 < r) ∧ a + ↑a_1 * (↑b * Complex.I).exp = z) → Complex.abs (z - a) < r ∧ ¬z = a
Theorem: IsPreconnected.ball_diff_center
Proof state before:
case h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
⊢ Complex.abs (z - a) < r ∧ ¬z = a → ∃ a_2 b, (0 < a_2 ∧ a_2 < r) ∧ a + ↑a_2 * (↑b * Complex.I).exp = z
Tactic:
intro ⟨zr, za⟩
Proof state after:
case h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
zr : Complex.abs (z - a) < r
za : ¬z = a
⊢ ∃ a_1 b, (0 < a_1 ∧ a_1 < r) ∧ a + ↑a_1 * (↑b * Complex.I).exp = z
Theorem: IsPreconnected.ball_diff_center
Proof state before:
case h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
zr : Complex.abs (z - a) < r
za : ¬z = a
⊢ ∃ a_1 b, (0 < a_1 ∧ a_1 < r) ∧ a + ↑a_1 * (↑b * Complex.I).exp = z
Tactic:
use abs (z - a), Complex.arg (z - a)
Proof state after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
zr : Complex.abs (z - a) < r
za : ¬z = a
⊢ (0 < Complex.abs (z - a) ∧ Complex.abs (z - a) < r) ∧ a + ↑(Complex.abs (z - a)) * (↑(z - a).arg * Complex.I).exp = z
Theorem: IsPreconnected.ball_diff_center
Proof state before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
zr : Complex.abs (z - a) < r
za : ¬z = a
⊢ (0 < Complex.abs (z - a) ∧ Complex.abs (z - a) < r) ∧ a + ↑(Complex.abs (z - a)) * (↑(z - a).arg * Complex.I).exp = z
Tactic:
simp only [AbsoluteValue.pos_iff, Ne, Complex.abs_mul_exp_arg_mul_I,
  add_sub_cancel, eq_self_iff_true, sub_eq_zero, za, zr, not_false_iff, and_true_iff]
Proof state after:
no goals
Theorem: IsPreconnected.ball_diff_center
Proof state before:
case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
⊢ (∃ a_1 b, (0 < a_1 ∧ a_1 < r) ∧ a + ↑a_1 * (↑b * Complex.I).exp = z) → Complex.abs (z - a) < r ∧ ¬z = a
Tactic:
intro ⟨s, t, ⟨s0, sr⟩, e⟩
Proof state after:
case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
s t : ℝ
s0 : 0 < s
sr : s < r
e : a + ↑s * (↑t * Complex.I).exp = z
⊢ Complex.abs (z - a) < r ∧ ¬z = a