case intro.intro.intro
α : Type u_1
β : Type ?u.147561
γ : Type ?u.147564
γ₂ : Type ?u.147567
δ : Type ?u.147570
ι : Sort y
t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
S : Set (Set α)
hSo : ∀ (t : Set α), t ∈ S → IsOpen t
hSc : Set.Countable S
⊢ MeasurableSet (⋂₀ S)
α : Type u_1
β : Type ?u.147561
γ : Type ?u.147564
γ₂ : Type ?u.147567
δ : Type ?u.147570
ι : Sort y
s t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
h : IsGδ s
⊢ MeasurableSet s
rcases h with ⟨S, hSo, hSc, rfl⟩
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.147561
γ : Type ?u.147564
γ₂ : Type ?u.147567
δ : Type ?u.147570
ι : Sort y
t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
S : Set (Set α)
hSo : ∀ (t : Set α), t ∈ S → IsOpen t
hSc : Set.Countable S
⊢ MeasurableSet (⋂₀ S)
exact MeasurableSet.sInter hSc fun t ht => (hSo t ht).measurableSet