α : Type u_1
β : Type ?u.6095
γ : Type ?u.6098
ι : Type ?u.6101
inst✝ : TopologicalSpace α
s t : Set α
hs : IsGδ s
ht : IsGδ t
⊢ IsGδ (⋂ (b : Bool), bif b then s else t)
α : Type u_1
β : Type ?u.6095
γ : Type ?u.6098
ι : Type ?u.6101
inst✝ : TopologicalSpace α
s t : Set α
hs : IsGδ s
ht : IsGδ t
⊢ IsGδ (s ∩ t)
rw [inter_eq_iInter]
no goals
α : Type u_1
β : Type ?u.6095
γ : Type ?u.6098
ι : Type ?u.6101
inst✝ : TopologicalSpace α
s t : Set α
hs : IsGδ s
ht : IsGδ t
⊢ IsGδ (⋂ (b : Bool), bif b then s else t)
exact isGδ_iInter (Bool.forall_bool.2 ⟨ht, hs⟩)