α : Type u_2
β : Type u_1
γ : Type ?u.23152
ι : Type ?u.23155
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set β
f : (x : β) → x ∈ S → Set α
ho : ∀ (s : β) (H : s ∈ S), IsGδ (f s H)
hS : Set.Countable S
hd : ∀ (s : β) (H : s ∈ S), Dense (f s H)
⊢ Dense (⋂ (x : ↑S), f ↑x (_ : ↑x ∈ S))
α : Type u_2
β : Type u_1
γ : Type ?u.23152
ι : Type ?u.23155
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set β
f : (x : β) → x ∈ S → Set α
ho : ∀ (s : β) (H : s ∈ S), IsGδ (f s H)
hS : Set.Countable S
hd : ∀ (s : β) (H : s ∈ S), Dense (f s H)
⊢ Dense (⋂ (s : β) (h : s ∈ S), f s h)
rw [biInter_eq_iInter]
α : Type u_2
β : Type u_1
γ : Type ?u.23152
ι : Type ?u.23155
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set β
f : (x : β) → x ∈ S → Set α
ho : ∀ (s : β) (H : s ∈ S), IsGδ (f s H)
hS : Set.Countable S
hd : ∀ (s : β) (H : s ∈ S), Dense (f s H)
this : Encodable ↑S
⊢ Dense (⋂ (x : ↑S), f ↑x (_ : ↑x ∈ S))
α : Type u_2
β : Type u_1
γ : Type ?u.23152
ι : Type ?u.23155
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set β
f : (x : β) → x ∈ S → Set α
ho : ∀ (s : β) (H : s ∈ S), IsGδ (f s H)
hS : Set.Countable S
hd : ∀ (s : β) (H : s ∈ S), Dense (f s H)
⊢ Dense (⋂ (x : ↑S), f ↑x (_ : ↑x ∈ S))
haveI := hS.toEncodable
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.23152
ι : Type ?u.23155
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set β
f : (x : β) → x ∈ S → Set α
ho : ∀ (s : β) (H : s ∈ S), IsGδ (f s H)
hS : Set.Countable S
hd : ∀ (s : β) (H : s ∈ S), Dense (f s H)
this : Encodable ↑S
⊢ Dense (⋂ (x : ↑S), f ↑x (_ : ↑x ∈ S))
exact dense_iInter_of_Gδ (fun s => ho s s.2) fun s => hd s s.2