case h
α : Type u_1
β : Type ?u.36119
γ : Type ?u.36122
δ : Type ?u.36125
δ' : Type ?u.36128
ι : Sort u_2
s✝ t u : Set α
m : ι → MeasurableSpace α
s : Set α
⊢ MeasurableSet s ↔ MeasurableSet s
α : Type u_1
β : Type ?u.36119
γ : Type ?u.36122
δ : Type ?u.36125
δ' : Type ?u.36128
ι : Sort u_2
s t u : Set α
m : ι → MeasurableSpace α
⊢ (⨆ (n : ι), m n) = generateFrom {s | ∃ n, MeasurableSet s}
ext s
case h
α : Type u_1
β : Type ?u.36119
γ : Type ?u.36122
δ : Type ?u.36125
δ' : Type ?u.36128
ι : Sort u_2
s✝ t u : Set α
m : ι → MeasurableSpace α
s : Set α
⊢ GenerateMeasurable {s | ∃ i, MeasurableSet s} s ↔ MeasurableSet s
case h
α : Type u_1
β : Type ?u.36119
γ : Type ?u.36122
δ : Type ?u.36125
δ' : Type ?u.36128
ι : Sort u_2
s✝ t u : Set α
m : ι → MeasurableSpace α
s : Set α
⊢ MeasurableSet s ↔ MeasurableSet s
rw [measurableSet_iSup]
no goals
case h
α : Type u_1
β : Type ?u.36119
γ : Type ?u.36122
δ : Type ?u.36125
δ' : Type ?u.36128
ι : Sort u_2
s✝ t u : Set α
m : ι → MeasurableSpace α
s : Set α
⊢ GenerateMeasurable {s | ∃ i, MeasurableSet s} s ↔ MeasurableSet s
rfl