[GOAL]
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)
[PROOFSTEP]
rw [← preimage_smul_inv]
[GOAL]
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)
[PROOFSTEP]
exact measurable_const_smul _ hs
[GOAL]
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)
[PROOFSTEP]
rw [← preimage_smul_inv₀ ha]
[GOAL]
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)
[PROOFSTEP]
exact measurable_const_smul _ hs
[GOAL]
G₀ : Type u_1
α : Type u_2
inst✝⁶ : GroupWithZero G₀
inst✝⁵ : Zero α
inst✝⁴ : MulActionWithZero G₀ α
inst✝³ : MeasurableSpace G₀
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSMul G₀ α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet s
a : G₀
⊢ MeasurableSet (a • s)
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case inl
G₀ : Type u_1
α : Type u_2
inst✝⁶ : GroupWithZero G₀
inst✝⁵ : Zero α
inst✝⁴ : MulActionWithZero G₀ α
inst✝³ : MeasurableSpace G₀
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSMul G₀ α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (0 • s)
case inr
G₀ : Type u_1
α : Type u_2
inst✝⁶ : GroupWithZero G₀
inst✝⁵ : Zero α
inst✝⁴ : MulActionWithZero G₀ α
inst✝³ : MeasurableSpace G₀
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSMul G₀ α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet s
a : G₀
ha : a ≠ 0
⊢ MeasurableSet (a • s)
[PROOFSTEP]
exacts [(subsingleton_zero_smul_set s).measurableSet, hs.const_smul_of_ne_zero ha]
