α : Type u_1
β : Type ?u.8090
γ : Type ?u.8093
δ : Type ?u.8096
δ' : Type ?u.8099
ι : Sort ?u.8102
s✝ t u : Set α
m : MeasurableSpace α
s : Set (Set α)
hs : Set.Countable s
h : ∀ (t : Set α), t ∈ s → MeasurableSet t
⊢ MeasurableSet (⋂ (i : Set α) (_ : i ∈ s), i)
α : Type u_1
β : Type ?u.8090
γ : Type ?u.8093
δ : Type ?u.8096
δ' : Type ?u.8099
ι : Sort ?u.8102
s✝ t u : Set α
m : MeasurableSpace α
s : Set (Set α)
hs : Set.Countable s
h : ∀ (t : Set α), t ∈ s → MeasurableSet t
⊢ MeasurableSet (⋂₀ s)
rw [sInter_eq_biInter]
no goals
α : Type u_1
β : Type ?u.8090
γ : Type ?u.8093
δ : Type ?u.8096
δ' : Type ?u.8099
ι : Sort ?u.8102
s✝ t u : Set α
m : MeasurableSpace α
s : Set (Set α)
hs : Set.Countable s
h : ∀ (t : Set α), t ∈ s → MeasurableSet t
⊢ MeasurableSet (⋂ (i : Set α) (_ : i ∈ s), i)
exact MeasurableSet.biInter hs h