α : Type u_1
β : Type ?u.13908
γ : Type ?u.13911
δ : Type ?u.13914
δ' : Type ?u.13917
ι : Sort ?u.13920
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : Set.Countable s
⊢ MeasurableSet (⋃ (x : α) (_ : x ∈ s), {x})
α : Type u_1
β : Type ?u.13908
γ : Type ?u.13911
δ : Type ?u.13914
δ' : Type ?u.13917
ι : Sort ?u.13920
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : Set.Countable s
⊢ MeasurableSet s
rw [← biUnion_of_singleton s]
no goals
α : Type u_1
β : Type ?u.13908
γ : Type ?u.13911
δ : Type ?u.13914
δ' : Type ?u.13917
ι : Sort ?u.13920
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : Set.Countable s
⊢ MeasurableSet (⋃ (x : α) (_ : x ∈ s), {x})
exact .biUnion hs fun b _ => .singleton b