internlm/Lean-Github huggingface dataset:
Theorem: IsPreconnected.open_diff
Proof state before:
case right
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)
x : X
u c : Set X
m : x ∈ s
xt : x ∈ t
cn : c ∈ 𝓝[tᶜ] x
cu : c ⊆ u
⊢ u ∈ 𝓝[tᶜ] x
Tactic:
exact Filter.mem_of_superset cn cu
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
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
⊢ s ⊆ f u ∪ f v
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
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
x : X
m : x ∈ s
⊢ x ∈ f u ∪ f v
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
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
x : X
m : x ∈ s
⊢ x ∈ f u ∪ f v
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
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
x : X
m : x ∈ s
xt : x ∉ t
⊢ x ∈ f u ∪ f v

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
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
x : X
m : x ∈ s
xt : ¬x ∉ t
⊢ x ∈ f u ∪ f v
Theorem: IsPreconnected.open_diff
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
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
x : X
m : x ∈ s
xt : x ∉ t
⊢ x ∈ f u ∪ f v

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
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
x : X
m : x ∈ s
xt : ¬x ∉ t
⊢ x ∈ f u ∪ f v
Tactic:
exact union_subset_union (mono _) (mono _) (suv (mem_diff_of_mem m 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
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
x : X
m : x ∈ s
xt : ¬x ∉ t
⊢ x ∈ f u ∪ f v
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
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
x : X
m : x ∈ s
xt : ¬x ∉ t
⊢ x ∈ f u ∪ f v
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
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
x : X
m : x ∈ s
xt : x ∈ t
⊢ x ∈ f u ∪ f v
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
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
x : X
m : x ∈ s
xt : x ∈ t
⊢ x ∈ f u ∪ f v
Tactic:
rcases ts.loc x s xt (so.mem_nhds m) with ⟨c, cst, cn, cp⟩
Proof state after:
case neg.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
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
x : X
m : x ∈ s
xt : x ∈ t
c : Set X
cst : c ⊆ s \ t
cn : c ∈ 𝓝[tᶜ] x
cp : IsPreconnected c
⊢ x ∈ f u ∪ f v
Theorem: IsPreconnected.open_diff
Proof state before:
case neg.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
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
x : X
m : x ∈ s
xt : x ∈ t
c : Set X
cst : c ⊆ s \ t
cn : c ∈ 𝓝[tᶜ] x
cp : IsPreconnected c
⊢ x ∈ f u ∪ f v
Tactic:
have d := inter_subset_inter_left (u ∩ v) cst
Proof state after:
case neg.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
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
x : X
m : x ∈ s
xt : x ∈ t
c : Set X
cst : c ⊆ s \ t
cn : c ∈ 𝓝[tᶜ] x
cp : IsPreconnected c
d : c ∩ (u ∩ v) ⊆ s \ t ∩ (u ∩ v)
⊢ x ∈ f u ∪ f v
Theorem: IsPreconnected.open_diff
Proof state before:
case neg.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
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
x : X
m : x ∈ s
xt : x ∈ t
c : Set X
cst : c ⊆ s \ t
cn : c ∈ 𝓝[tᶜ] x
cp : IsPreconnected c
d : c ∩ (u ∩ v) ⊆ s \ t ∩ (u ∩ v)
⊢ x ∈ f u ∪ f v
Tactic:
rw [duv, subset_empty_iff] at d
Proof state after:
case neg.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
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
x : X
m : x ∈ s
xt : x ∈ t
c : Set X
cst : c ⊆ s \ t
cn : c ∈ 𝓝[tᶜ] x
cp : IsPreconnected c
d : c ∩ (u ∩ v) = ∅
⊢ x ∈ f u ∪ f v
Theorem: IsPreconnected.open_diff
Proof state before:
case neg.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
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
x : X
m : x ∈ s
xt : x ∈ t
c : Set X
cst : c ⊆ s \ t
cn : c ∈ 𝓝[tᶜ] x
cp : IsPreconnected c
d : c ∩ (u ∩ v) = ∅
⊢ x ∈ f u ∪ f v
Tactic:
cases' isPreconnected_iff_subset_of_disjoint.mp cp u v uo vo (_root_.trans cst suv) d with cu cv
Proof state after:
case neg.intro.intro.intro.inl
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
x : X
m : x ∈ s
xt : x ∈ t
c : Set X
cst : c ⊆ s \ t
cn : c ∈ 𝓝[tᶜ] x
cp : IsPreconnected c
d : c ∩ (u ∩ v) = ∅
cu : c ⊆ u
⊢ x ∈ f u ∪ f v

case neg.intro.intro.intro.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
x : X
m : x ∈ s
xt : x ∈ t
c : Set X
cst : c ⊆ s \ t
cn : c ∈ 𝓝[tᶜ] x
cp : IsPreconnected c
d : c ∩ (u ∩ v) = ∅
cv : c ⊆ v
⊢ x ∈ f u ∪ f v
Theorem: IsPreconnected.open_diff
Proof state before:
case neg.intro.intro.intro.inl
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
x : X
m : x ∈ s
xt : x ∈ t
c : Set X
cst : c ⊆ s \ t
cn : c ∈ 𝓝[tᶜ] x
cp : IsPreconnected c
d : c ∩ (u ∩ v) = ∅
cu : c ⊆ u
⊢ x ∈ f u ∪ f v

case neg.intro.intro.intro.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
x : X
m : x ∈ s
xt : x ∈ t
c : Set X
cst : c ⊆ s \ t
cn : c ∈ 𝓝[tᶜ] x
cp : IsPreconnected c
d : c ∩ (u ∩ v) = ∅
cv : c ⊆ v
⊢ x ∈ f u ∪ f v
Tactic:
exact subset_union_left _ _ (mem m xt cn cu)
Proof state after:
case neg.intro.intro.intro.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
x : X
m : x ∈ s
xt : x ∈ t
c : Set X
cst : c ⊆ s \ t
cn : c ∈ 𝓝[tᶜ] x
cp : IsPreconnected c
d : c ∩ (u ∩ v) = ∅
cv : c ⊆ v
⊢ x ∈ f u ∪ f v
Theorem: IsPreconnected.open_diff
Proof state before:
case neg.intro.intro.intro.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
x : X
m : x ∈ s
xt : x ∈ t
c : Set X
cst : c ⊆ s \ t
cn : c ∈ 𝓝[tᶜ] x
cp : IsPreconnected c
d : c ∩ (u ∩ v) = ∅
cv : c ⊆ v
⊢ x ∈ f u ∪ f v
Tactic:
exact subset_union_right _ _ (mem m xt cn cv)
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
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
⊢ ∀ {u : Set X}, f u \ t ⊆ u
Tactic:
intro u 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
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
u : Set X
x : X
m : x ∈ f u \ t
⊢ x ∈ 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
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
u : Set X
x : X
m : x ∈ f u \ t
⊢ x ∈ u
Tactic:
simp only [mem_diff, mem_union, mem_setOf, ← hf] at 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
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
u : Set X
x : X
m : (x ∈ u ∨ x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u) ∧ x ∉ t
⊢ x ∈ 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
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
u : Set X
x : X
m : (x ∈ u ∨ x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u) ∧ x ∉ t
⊢ x ∈ u
Tactic:
simp only [m.2, false_and_iff, and_false_iff, or_false_iff, not_false_iff, and_true_iff] at 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
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
u : Set X
x : X
m : x ∈ u
⊢ x ∈ u