α : Type u_2
β : Type u_1
γ : Type ?u.22697
ι : Type ?u.22700
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable β
f : β → Set α
ho : ∀ (s : β), IsGδ (f s)
hd : ∀ (s : β), Dense (f s)
⊢ Dense (⋂₀ range fun s => f s)
α : Type u_2
β : Type u_1
γ : Type ?u.22697
ι : Type ?u.22700
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable β
f : β → Set α
ho : ∀ (s : β), IsGδ (f s)
hd : ∀ (s : β), Dense (f s)
⊢ Dense (⋂ (s : β), f s)
rw [← sInter_range]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.22697
ι : Type ?u.22700
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable β
f : β → Set α
ho : ∀ (s : β), IsGδ (f s)
hd : ∀ (s : β), Dense (f s)
⊢ Dense (⋂₀ range fun s => f s)
exact dense_sInter_of_Gδ (forall_range_iff.2 ‹_›) (countable_range _) (forall_range_iff.2 ‹_›)