Pointwise set operations on MeasurableSets #
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_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_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_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)