α : Type u_1
β : Type u_2
γ : Type ?u.378292
δ : Type ?u.378295
δ' : Type ?u.378298
ι : Sort uι
s t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace α
⊢ MeasurableSet (Sum.inl '' univ)
α : Type u_1
β : Type u_2
γ : Type ?u.378292
δ : Type ?u.378295
δ' : Type ?u.378298
ι : Sort uι
s t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace α
⊢ MeasurableSet (range Sum.inl)
rw [← image_univ]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.378292
δ : Type ?u.378295
δ' : Type ?u.378298
ι : Sort uι
s t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace α
⊢ MeasurableSet (Sum.inl '' univ)
exact MeasurableSet.univ.inl_image