α : Type u_1
β : Type u_2
γ : Type ?u.380657
δ : Type ?u.380660
δ' : Type ?u.380663
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hf : MeasurableEmbedding f
⊢ MeasurableSet (f '' univ)
α : Type u_1
β : Type u_2
γ : Type ?u.380657
δ : Type ?u.380660
δ' : Type ?u.380663
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hf : MeasurableEmbedding f
⊢ MeasurableSet (range f)
rw [← image_univ]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.380657
δ : Type ?u.380660
δ' : Type ?u.380663
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hf : MeasurableEmbedding f
⊢ MeasurableSet (f '' univ)
exact hf.measurableSet_image' MeasurableSet.univ