G : Type u_1
α : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSMul G α
s : Set α
hs : MeasurableSet s
a : G
⊢ MeasurableSet ((fun x => a⁻¹ • x) ⁻¹' s)
G : Type u_1
α : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSMul G α
s : Set α
hs : MeasurableSet s
a : G
⊢ MeasurableSet (a • s)
rw [← preimage_smul_inv]
no goals
G : Type u_1
α : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSMul G α
s : Set α
hs : MeasurableSet s
a : G
⊢ MeasurableSet ((fun x => a⁻¹ • x) ⁻¹' s)
exact measurable_const_smul _ hs