internlm/Lean-Github huggingface dataset:
Theorem: IsPreconnected.open_diff
Proof state before:
case inl.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
duv : 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
disj : s ∩ (f u ∩ f v) = ∅
su : s ⊆ f u
⊢ s \ t ⊆ u

case inr
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
duv : 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
disj : s ∩ (f u ∩ f v) = ∅
sv : s ⊆ f v
⊢ s \ t ⊆ u ∨ s \ t ⊆ v
Tactic:
exact _root_.trans (diff_subset_diff_left su) fdiff
Proof state after:
case inr
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
duv : 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
disj : s ∩ (f u ∩ f v) = ∅
sv : s ⊆ f v
⊢ s \ t ⊆ u ∨ s \ t ⊆ v
Theorem: IsPreconnected.open_diff
Proof state before:
case inr
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
duv : 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
disj : s ∩ (f u ∩ f v) = ∅
sv : s ⊆ f v
⊢ s \ t ⊆ u ∨ s \ t ⊆ v
Tactic:
right
Proof state after:
case inr.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
duv : 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
disj : s ∩ (f u ∩ f v) = ∅
sv : s ⊆ f v
⊢ s \ t ⊆ v
Theorem: IsPreconnected.open_diff
Proof state before:
case inr.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
duv : 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
disj : s ∩ (f u ∩ f v) = ∅
sv : s ⊆ f v
⊢ s \ t ⊆ v
Tactic:
exact _root_.trans (diff_subset_diff_left sv) fdiff
Proof state after:
no goals
Theorem: IsPreconnected.open_diff
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
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
duv : 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
⊢ ∀ (u : Set X), u ⊆ f u
Tactic:
rw [← hf]
Proof state after:
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
duv : 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
⊢ ∀ (u : Set X), u ⊆ (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) u
Theorem: IsPreconnected.open_diff
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
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
duv : 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
⊢ ∀ (u : Set X), u ⊆ (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) u
Tactic:
exact fun _ ↦ subset_union_left _ _
Proof state after:
no goals
Theorem: IsPreconnected.open_diff
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
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
duv : 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
⊢ ∀ {u : Set X}, IsOpen u → IsOpen (f u)
Tactic:
intro u o
Proof state after:
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
duv : 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
u : Set X
o : IsOpen u
⊢ IsOpen (f u)
Theorem: IsPreconnected.open_diff
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
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
duv : 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
u : Set X
o : IsOpen u
⊢ IsOpen (f u)
Tactic:
rw [isOpen_iff_eventually]
Proof state after:
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
duv : 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
u : Set X
o : IsOpen u
⊢ ∀ x ∈ f u, ∀ᶠ (y : X) in 𝓝 x, y ∈ f u
Theorem: IsPreconnected.open_diff
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
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
duv : 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
u : Set X
o : IsOpen u
⊢ ∀ x ∈ f u, ∀ᶠ (y : X) in 𝓝 x, y ∈ f u
Tactic:
intro x m
Proof state after:
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
duv : 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
u : Set X
o : IsOpen u
x : X
m : x ∈ f u
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ f u
Theorem: IsPreconnected.open_diff
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
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
duv : 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
u : Set X
o : IsOpen u
x : X
m : x ∈ f u
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ f u
Tactic:
by_cases xu : x ∈ u
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
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
duv : 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
u : Set X
o : IsOpen u
x : X
m : x ∈ f u
xu : x ∈ u
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ f u

case neg
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
duv : 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
u : Set X
o : IsOpen u
x : X
m : x ∈ f u
xu : x ∉ u
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ f u
Theorem: IsPreconnected.open_diff
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
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
duv : 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
u : Set X
o : IsOpen u
x : X
m : x ∈ f u
xu : x ∉ u
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ f u
Tactic:
by_cases xt : x ∉ t
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
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
duv : 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
u : Set X
o : IsOpen u
x : X
m : x ∈ f u
xu : x ∉ u
xt : x ∉ t
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ f u

case neg
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
duv : 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
u : Set X
o : IsOpen u
x : X
m : x ∈ f u
xu : x ∉ u
xt : ¬x ∉ t
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ f u
Theorem: IsPreconnected.open_diff
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
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
duv : 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
u : Set X
o : IsOpen u
x : X
m : x ∈ f u
xu : x ∉ u
xt : ¬x ∉ t
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ f u
Tactic:
simp only [not_not] at xt
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
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
duv : 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
u : Set X
o : IsOpen u
x : X
m : x ∈ f u
xu : x ∉ u
xt : x ∈ t
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ f u
Theorem: IsPreconnected.open_diff
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
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
duv : 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
u : Set X
o : IsOpen u
x : X
m : x ∈ f u
xu : x ∉ u
xt : x ∈ t
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ f u
Tactic:
have n := m
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
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
duv : 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
u : Set X
o : IsOpen u
x : X
m : x ∈ f u
xu : x ∉ u
xt : x ∈ t
n : x ∈ f u
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ f u
Theorem: IsPreconnected.open_diff
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
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
duv : 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
u : Set X
o : IsOpen u
x : X
m : x ∈ f u
xu : x ∉ u
xt : x ∈ t
n : x ∈ f u
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ f u
Tactic:
simp only [mem_union, xt, xu, false_or_iff, true_and_iff, mem_setOf,
  eventually_nhdsWithin_iff, ← hf] at n
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
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
duv : 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
u : Set X
o : IsOpen u
x : X
m : x ∈ f u
xu : x ∉ u
xt : x ∈ t
n : x ∈ s ∧ ∀ᶠ (x : X) in 𝓝 x, x ∈ tᶜ → x ∈ u
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ f u
Theorem: IsPreconnected.open_diff
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
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
duv : 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
u : Set X
o : IsOpen u
x : X
m : x ∈ f u
xu : x ∉ u
xt : x ∈ t
n : x ∈ s ∧ ∀ᶠ (x : X) in 𝓝 x, x ∈ tᶜ → x ∈ u
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ f u
Tactic:
refine (so.eventually_mem n.1).mp (n.2.eventually_nhds.mp (eventually_of_forall fun y n m ↦ ?_))
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
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
duv : 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
u : Set X
o : IsOpen u
x : X
m✝ : x ∈ f u
xu : x ∉ u
xt : x ∈ t
n✝ : x ∈ s ∧ ∀ᶠ (x : X) in 𝓝 x, x ∈ tᶜ → x ∈ u
y : X
n : ∀ᶠ (x : X) in 𝓝 y, x ∈ tᶜ → x ∈ u
m : y ∈ s
⊢ y ∈ f u
Theorem: IsPreconnected.open_diff
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
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
duv : 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
u : Set X
o : IsOpen u
x : X
m✝ : x ∈ f u
xu : x ∉ u
xt : x ∈ t
n✝ : x ∈ s ∧ ∀ᶠ (x : X) in 𝓝 x, x ∈ tᶜ → x ∈ u
y : X
n : ∀ᶠ (x : X) in 𝓝 y, x ∈ tᶜ → x ∈ u
m : y ∈ s
⊢ y ∈ f u
Tactic:
by_cases yt : y ∈ t
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
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
duv : 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
u : Set X
o : IsOpen u
x : X
m✝ : x ∈ f u
xu : x ∉ u
xt : x ∈ t
n✝ : x ∈ s ∧ ∀ᶠ (x : X) in 𝓝 x, x ∈ tᶜ → x ∈ u
y : X
n : ∀ᶠ (x : X) in 𝓝 y, x ∈ tᶜ → x ∈ u
m : y ∈ s
yt : y ∈ t
⊢ y ∈ f u

case neg
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
duv : 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
u : Set X
o : IsOpen u
x : X
m✝ : x ∈ f u
xu : x ∉ u
xt : x ∈ t
n✝ : x ∈ s ∧ ∀ᶠ (x : X) in 𝓝 x, x ∈ tᶜ → x ∈ u
y : X
n : ∀ᶠ (x : X) in 𝓝 y, x ∈ tᶜ → x ∈ u
m : y ∈ s
yt : y ∉ t
⊢ y ∈ f u