no goals
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.129204
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
x : α
s : Finset α
h : ¬x ∈ s
⊢ SeparatedNhds {x} ↑s
exact_mod_cast finset_disjoint_finset_opens_of_t2 {x} s (Finset.disjoint_singleton_left.mpr h)