# Pointwise set operations on `MeasurableSet`

s #

In this file we prove several versions of the following fact: if `s`

is a measurable set, then so is
`a • s`

. Note that the pointwise product of two measurable sets need not be measurable, so there is
no `MeasurableSet.mul`

etc.

theorem
MeasurableSet.const_vadd
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
[MeasurableSpace G]
[MeasurableSpace α]
[MeasurableVAdd G α]
{s : Set α}
(hs : MeasurableSet s)
(a : G)
:

MeasurableSet (a +ᵥ s)

theorem
MeasurableSet.const_smul
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
[MeasurableSpace G]
[MeasurableSpace α]
[MeasurableSMul G α]
{s : Set α}
(hs : MeasurableSet s)
(a : G)
:

MeasurableSet (a • s)

theorem
MeasurableSet.const_smul_of_ne_zero
{G₀ : Type u_1}
{α : Type u_2}
[GroupWithZero G₀]
[MulAction G₀ α]
[MeasurableSpace G₀]
[MeasurableSpace α]
[MeasurableSMul G₀ α]
{s : Set α}
(hs : MeasurableSet s)
{a : G₀}
(ha : a ≠ 0)
:

MeasurableSet (a • s)

theorem
MeasurableSet.const_smul₀
{G₀ : Type u_1}
{α : Type u_2}
[GroupWithZero G₀]
[Zero α]
[MulActionWithZero G₀ α]
[MeasurableSpace G₀]
[MeasurableSpace α]
[MeasurableSMul G₀ α]
[MeasurableSingletonClass α]
{s : Set α}
(hs : MeasurableSet s)
(a : G₀)
:

MeasurableSet (a • s)