ι : Type ?u.3562
α : Type u_1
β : Type ?u.3568
γ : Type ?u.3571
m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
s : Set (Set α)
hs : Set.Countable s
h : ∀ (t : Set α), t ∈ s → NullMeasurableSet t
⊢ NullMeasurableSet (⋃ (i : Set α) (_ : i ∈ s), i)
ι : Type ?u.3562
α : Type u_1
β : Type ?u.3568
γ : Type ?u.3571
m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
s : Set (Set α)
hs : Set.Countable s
h : ∀ (t : Set α), t ∈ s → NullMeasurableSet t
⊢ NullMeasurableSet (⋃₀ s)
rw [sUnion_eq_biUnion]
no goals
ι : Type ?u.3562
α : Type u_1
β : Type ?u.3568
γ : Type ?u.3571
m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
s : Set (Set α)
hs : Set.Countable s
h : ∀ (t : Set α), t ∈ s → NullMeasurableSet t
⊢ NullMeasurableSet (⋃ (i : Set α) (_ : i ∈ s), i)
exact MeasurableSet.biUnion hs h