α : Type u_1
β : Type ?u.23922
γ : Type ?u.23925
ι : Type ?u.23928
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s t : Set α
hs : IsGδ s
ht : IsGδ t
hsc : Dense s
htc : Dense t
⊢ Dense (⋂ (b : Bool), bif b then s else t)
α : Type u_1
β : Type ?u.23922
γ : Type ?u.23925
ι : Type ?u.23928
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s t : Set α
hs : IsGδ s
ht : IsGδ t
hsc : Dense s
htc : Dense t
⊢ Dense (s ∩ t)
rw [inter_eq_iInter]
no goals
α : Type u_1
β : Type ?u.23922
γ : Type ?u.23925
ι : Type ?u.23928
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s t : Set α
hs : IsGδ s
ht : IsGδ t
hsc : Dense s
htc : Dense t
⊢ Dense (⋂ (b : Bool), bif b then s else t)
apply dense_iInter_of_Gδ <;> simp [Bool.forall_bool, *]