α : Type u_2
β : Type u_1
γ : Type ?u.14090
ι : Type ?u.14093
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable β
f : β → Set α
ho : ∀ (s : β), IsOpen (f s)
hd : ∀ (s : β), Dense (f s)
⊢ Dense (⋂₀ range fun s => f s)
α : Type u_2
β : Type u_1
γ : Type ?u.14090
ι : Type ?u.14093
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable β
f : β → Set α
ho : ∀ (s : β), IsOpen (f s)
hd : ∀ (s : β), Dense (f s)
⊢ Dense (⋂ (s : β), f s)
rw [← sInter_range]
case ho
α : Type u_2
β : Type u_1
γ : Type ?u.14090
ι : Type ?u.14093
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable β
f : β → Set α
ho : ∀ (s : β), IsOpen (f s)
hd : ∀ (s : β), Dense (f s)
⊢ ∀ (s : Set α), (s ∈ range fun s => f s) → IsOpen s

case hS
α : Type u_2
β : Type u_1
γ : Type ?u.14090
ι : Type ?u.14093
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable β
f : β → Set α
ho : ∀ (s : β), IsOpen (f s)
hd : ∀ (s : β), Dense (f s)
⊢ Set.Countable (range fun s => f s)

case hd
α : Type u_2
β : Type u_1
γ : Type ?u.14090
ι : Type ?u.14093
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable β
f : β → Set α
ho : ∀ (s : β), IsOpen (f s)
hd : ∀ (s : β), Dense (f s)
⊢ ∀ (s : Set α), (s ∈ range fun s => f s) → Dense s
α : Type u_2
β : Type u_1
γ : Type ?u.14090
ι : Type ?u.14093
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable β
f : β → Set α
ho : ∀ (s : β), IsOpen (f s)
hd : ∀ (s : β), Dense (f s)
⊢ Dense (⋂₀ range fun s => f s)
apply dense_sInter_of_open
no goals
case ho
α : Type u_2
β : Type u_1
γ : Type ?u.14090
ι : Type ?u.14093
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable β
f : β → Set α
ho : ∀ (s : β), IsOpen (f s)
hd : ∀ (s : β), Dense (f s)
⊢ ∀ (s : Set α), (s ∈ range fun s => f s) → IsOpen s
rwa [forall_range_iff]
no goals
case hS
α : Type u_2
β : Type u_1
γ : Type ?u.14090
ι : Type ?u.14093
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable β
f : β → Set α
ho : ∀ (s : β), IsOpen (f s)
hd : ∀ (s : β), Dense (f s)
⊢ Set.Countable (range fun s => f s)
exact countable_range _
no goals
case hd
α : Type u_2
β : Type u_1
γ : Type ?u.14090
ι : Type ?u.14093
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable β
f : β → Set α
ho : ∀ (s : β), IsOpen (f s)
hd : ∀ (s : β), Dense (f s)
⊢ ∀ (s : Set α), (s ∈ range fun s => f s) → Dense s
rwa [forall_range_iff]