α : Type u_1
β : Type ?u.31417
γ : Type ?u.31420
δ : Type ?u.31423
δ' : Type ?u.31426
ι : Sort ?u.31429
s✝ t u : Set α
ms : Set (MeasurableSpace α)
s : Set α
⊢ GenerateMeasurable (⋃₀ ((fun m => {t | MeasurableSet t}) '' ms)) s ↔
    GenerateMeasurable {s | ∃ m, m ∈ ms ∧ MeasurableSet s} s
α : Type u_1
β : Type ?u.31417
γ : Type ?u.31420
δ : Type ?u.31423
δ' : Type ?u.31426
ι : Sort ?u.31429
s✝ t u : Set α
ms : Set (MeasurableSpace α)
s : Set α
⊢ MeasurableSet s ↔ GenerateMeasurable {s | ∃ m, m ∈ ms ∧ MeasurableSet s} s
change GenerateMeasurable (⋃₀ _) _ ↔ _
no goals
α : Type u_1
β : Type ?u.31417
γ : Type ?u.31420
δ : Type ?u.31423
δ' : Type ?u.31426
ι : Sort ?u.31429
s✝ t u : Set α
ms : Set (MeasurableSpace α)
s : Set α
⊢ GenerateMeasurable (⋃₀ ((fun m => {t | MeasurableSet t}) '' ms)) s ↔
    GenerateMeasurable {s | ∃ m, m ∈ ms ∧ MeasurableSet s} s
simp [← setOf_exists]