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