Pointwise set operations on measurable_sets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 measurable_set.mul etc.
theorem
measurable_set.const_smul
{G : Type u_1}
{α : Type u_2}
[group G]
[mul_action G α]
[measurable_space G]
[measurable_space α]
[has_measurable_smul G α]
{s : set α}
(hs : measurable_set s)
(a : G) :
measurable_set (a • s)
theorem
measurable_set.const_vadd
{G : Type u_1}
{α : Type u_2}
[add_group G]
[add_action G α]
[measurable_space G]
[measurable_space α]
[has_measurable_vadd G α]
{s : set α}
(hs : measurable_set s)
(a : G) :
measurable_set (a +ᵥ s)
theorem
measurable_set.const_smul_of_ne_zero
{G₀ : Type u_1}
{α : Type u_2}
[group_with_zero G₀]
[mul_action G₀ α]
[measurable_space G₀]
[measurable_space α]
[has_measurable_smul G₀ α]
{s : set α}
(hs : measurable_set s)
{a : G₀}
(ha : a ≠ 0) :
measurable_set (a • s)
theorem
measurable_set.const_smul₀
{G₀ : Type u_1}
{α : Type u_2}
[group_with_zero G₀]
[has_zero α]
[mul_action_with_zero G₀ α]
[measurable_space G₀]
[measurable_space α]
[has_measurable_smul G₀ α]
[measurable_singleton_class α]
{s : set α}
(hs : measurable_set s)
(a : G₀) :
measurable_set (a • s)