no goals
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.129636
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
s : Set α
hs : IsCompact s
x : α
hx : x ∈ sᶜ
u v : Set α
left✝ : IsOpen u
vo : IsOpen v
su : s ⊆ u
xv : {x} ⊆ v
uv : Disjoint u v
⊢ x ∈ v
simpa using xv