internlm/Lean-Github huggingface dataset:
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
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
Tactic:
simp only [mem_union, mem_setOf, eventually_nhdsWithin_iff, ← hf]
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 ∈ u ∨ y ∈ s ∧ y ∈ t ∧ ∀ᶠ (x : X) in 𝓝 y, x ∈ tᶜ → x ∈ 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
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
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 ∈ u ∨ y ∈ s ∧ y ∈ t ∧ ∀ᶠ (x : X) in 𝓝 y, x ∈ tᶜ → x ∈ 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
Tactic:
right
Proof state after:
case pos.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
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 ∈ s ∧ y ∈ t ∧ ∀ᶠ (x : X) in 𝓝 y, x ∈ tᶜ → x ∈ 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
Theorem: IsPreconnected.open_diff
Proof state before:
case pos.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
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 ∈ s ∧ y ∈ t ∧ ∀ᶠ (x : X) in 𝓝 y, x ∈ tᶜ → x ∈ 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
Tactic:
use m, yt, 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
n : ∀ᶠ (x : X) in 𝓝 y, x ∈ tᶜ → x ∈ u
m : y ∈ s
yt : y ∉ t
⊢ 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
yt : y ∉ t
⊢ y ∈ f u
Tactic:
exact mono _ (n.self_of_nhds yt)
Proof state after:
no goals
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
u : Set X
o : IsOpen u
x : X
m : x ∈ f u
xu : x ∈ u
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ f u
Tactic:
rw [← hf]
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 ∈ (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) u
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
u : Set X
o : IsOpen u
x : X
m : x ∈ f u
xu : x ∈ u
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) u
Tactic:
exact (o.eventually_mem xu).mp (eventually_of_forall fun q m ↦ subset_union_left _ _ m)
Proof state after:
no goals
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
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:
contrapose xu
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
xt : x ∉ t
xu : ¬∀ᶠ (y : X) in 𝓝 x, y ∈ f u
⊢ ¬x ∉ u
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
u : Set X
o : IsOpen u
x : X
m : x ∈ f u
xt : x ∉ t
xu : ¬∀ᶠ (y : X) in 𝓝 x, y ∈ f u
⊢ ¬x ∉ u
Tactic:
clear xu
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
xt : x ∉ t
⊢ ¬x ∉ u
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
u : Set X
o : IsOpen u
x : X
m : x ∈ f u
xt : x ∉ t
⊢ ¬x ∉ u
Tactic:
simp only [mem_union, mem_setOf, xt, false_and_iff, and_false_iff, or_false_iff, ← hf] at m
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
xt : x ∉ t
m : x ∈ u
⊢ ¬x ∉ u
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
u : Set X
o : IsOpen u
x : X
xt : x ∉ t
m : x ∈ u
⊢ ¬x ∉ u
Tactic:
simp only [not_not]
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
xt : x ∉ t
m : x ∈ u
⊢ x ∈ u
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
u : Set X
o : IsOpen u
x : X
xt : x ∉ t
m : x ∈ u
⊢ x ∈ u
Tactic:
exact m
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)
⊢ ∀ {x : X} {u c : Set X}, x ∈ s → x ∈ t → c ∈ 𝓝[tᶜ] x → c ⊆ u → x ∈ f u
Tactic:
intro x u c m xt cn cu
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)
x : X
u c : Set X
m : x ∈ s
xt : x ∈ t
cn : c ∈ 𝓝[tᶜ] x
cu : c ⊆ u
⊢ x ∈ 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
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
⊢ x ∈ 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
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
⊢ x ∈ (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
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
⊢ x ∈ (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) u
Tactic:
right
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
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
⊢ x ∈ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}
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
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
⊢ x ∈ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}
Tactic:
use m, xt
Proof state after:
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
⊢ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u
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
⊢ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u
Tactic:
simp only [Filter.eventually_iff, setOf_mem_eq]
Proof state after:
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