Theorem: IsPreconnected.open_diff
Proof state before:
case 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
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 ∨ s \ t ⊆ v

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:
left
Proof state after:
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