α : Type u_1
β : Type ?u.11615
γ : Type ?u.11618
ι : Type ?u.11621
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
hs : Set.Countable s
⊢ IsGδ (⋂ (i : α) (_ : i ∈ s), {i}ᶜ)
α : Type u_1
β : Type ?u.11615
γ : Type ?u.11618
ι : Type ?u.11621
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
hs : Set.Countable s
⊢ IsGδ (sᶜ)
rw [← biUnion_of_singleton s, compl_iUnion₂]
no goals
α : Type u_1
β : Type ?u.11615
γ : Type ?u.11618
ι : Type ?u.11621
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
hs : Set.Countable s
⊢ IsGδ (⋂ (i : α) (_ : i ∈ s), {i}ᶜ)
exact isGδ_biInter hs fun x _ => isGδ_compl_singleton x