no goals
α : Type u_1
β : Type ?u.5691
γ : Type ?u.5694
ι : Type ?u.5697
inst✝ : TopologicalSpace α
S : Set (Set α)
h : ∀ (s : Set α), s ∈ S → IsGδ s
hS : Set.Countable S
⊢ IsGδ (⋂₀ S)
simpa only [sInter_eq_biInter] using isGδ_biInter hS h