α : Type u_1
β : Type u_2
γ : Type ?u.378457
δ : Type ?u.378460
δ' : Type ?u.378463
ι : Sort uι
s t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace α
⊢ MeasurableSet (Sum.inr '' univ)
α : Type u_1
β : Type u_2
γ : Type ?u.378457
δ : Type ?u.378460
δ' : Type ?u.378463
ι : Sort uι
s t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace α
⊢ MeasurableSet (range Sum.inr)
rw [← image_univ]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.378457
δ : Type ?u.378460
δ' : Type ?u.378463
ι : Sort uι
s t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace α
⊢ MeasurableSet (Sum.inr '' univ)
exact MeasurableSet.univ.inr_image