theorem PiBase.Set.not_mem_ext_iff {α : Type u} {a b : Set α} : a = b ↔ ∀ (x : α), x ∉ a ↔ x ∉ b

theorem PiBase.mem_isGδ_ex_nhds_separate {X : Type u} [TopologicalSpace X] {s : Set X} {x y : X} (hs : IsGδ s) (hx : x ∈ s) (hy : y ∉ s) : ∃ U ∈ nhds x, y ∉ U