α : Type u_1
β : Type ?u.6742
γ : Type ?u.6745
δ : Type ?u.6748
δ' : Type ?u.6751
ι : Sort ?u.6754
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.6742
γ : Type ?u.6745
δ : Type ?u.6748
δ' : Type ?u.6751
ι : Sort ?u.6754
s✝ t u : Set α
m : MeasurableSpace α
s : Set (Set α)
hs : Set.Countable s
h : ∀ (t : Set α), t ∈ s → MeasurableSet t
⊢ MeasurableSet (⋃₀ s)
rw [sUnion_eq_biUnion]
no goals
α : Type u_1
β : Type ?u.6742
γ : Type ?u.6745
δ : Type ?u.6748
δ' : Type ?u.6751
ι : Sort ?u.6754
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 .biUnion hs h