no goals
α : Type u_1
β : Type ?u.27858
γ : Type ?u.27861
δ : Type ?u.27864
δ' : Type ?u.27867
ι : Sort ?u.27870
s✝ t u : Set α
ms : Set (MeasurableSpace α)
s : Set α
⊢ s ∈ ⋂₀ ((fun m => {t | MeasurableSet t}) '' ms) ↔ ∀ (m : MeasurableSpace α), m ∈ ms → MeasurableSet s
simp