α : Type u_2
β : Type u_1
γ : Type ?u.13508
ι : Type ?u.13511
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set β
f : β → Set α
ho : ∀ (s : β), s ∈ S → IsOpen (f s)
hS : Set.Countable S
hd : ∀ (s : β), s ∈ S → Dense (f s)
⊢ Dense (⋂₀ ((fun s => f s) '' S))
α : Type u_2
β : Type u_1
γ : Type ?u.13508
ι : Type ?u.13511
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set β
f : β → Set α
ho : ∀ (s : β), s ∈ S → IsOpen (f s)
hS : Set.Countable S
hd : ∀ (s : β), s ∈ S → Dense (f s)
⊢ Dense (⋂ (s : β) (_ : s ∈ S), f s)
rw [← sInter_image]
case ho
α : Type u_2
β : Type u_1
γ : Type ?u.13508
ι : Type ?u.13511
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set β
f : β → Set α
ho : ∀ (s : β), s ∈ S → IsOpen (f s)
hS : Set.Countable S
hd : ∀ (s : β), s ∈ S → Dense (f s)
⊢ ∀ (s : Set α), s ∈ (fun s => f s) '' S → IsOpen s

case hS
α : Type u_2
β : Type u_1
γ : Type ?u.13508
ι : Type ?u.13511
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set β
f : β → Set α
ho : ∀ (s : β), s ∈ S → IsOpen (f s)
hS : Set.Countable S
hd : ∀ (s : β), s ∈ S → Dense (f s)
⊢ Set.Countable ((fun s => f s) '' S)

case hd
α : Type u_2
β : Type u_1
γ : Type ?u.13508
ι : Type ?u.13511
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set β
f : β → Set α
ho : ∀ (s : β), s ∈ S → IsOpen (f s)
hS : Set.Countable S
hd : ∀ (s : β), s ∈ S → Dense (f s)
⊢ ∀ (s : Set α), s ∈ (fun s => f s) '' S → Dense s
α : Type u_2
β : Type u_1
γ : Type ?u.13508
ι : Type ?u.13511
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set β
f : β → Set α
ho : ∀ (s : β), s ∈ S → IsOpen (f s)
hS : Set.Countable S
hd : ∀ (s : β), s ∈ S → Dense (f s)
⊢ Dense (⋂₀ ((fun s => f s) '' S))
apply dense_sInter_of_open
no goals
case ho
α : Type u_2
β : Type u_1
γ : Type ?u.13508
ι : Type ?u.13511
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set β
f : β → Set α
ho : ∀ (s : β), s ∈ S → IsOpen (f s)
hS : Set.Countable S
hd : ∀ (s : β), s ∈ S → Dense (f s)
⊢ ∀ (s : Set α), s ∈ (fun s => f s) '' S → IsOpen s
rwa [ball_image_iff]
no goals
case hS
α : Type u_2
β : Type u_1
γ : Type ?u.13508
ι : Type ?u.13511
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set β
f : β → Set α
ho : ∀ (s : β), s ∈ S → IsOpen (f s)
hS : Set.Countable S
hd : ∀ (s : β), s ∈ S → Dense (f s)
⊢ Set.Countable ((fun s => f s) '' S)
exact hS.image _
no goals
case hd
α : Type u_2
β : Type u_1
γ : Type ?u.13508
ι : Type ?u.13511
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set β
f : β → Set α
ho : ∀ (s : β), s ∈ S → IsOpen (f s)
hS : Set.Countable S
hd : ∀ (s : β), s ∈ S → Dense (f s)
⊢ ∀ (s : Set α), s ∈ (fun s => f s) '' S → Dense s
rwa [ball_image_iff]