mathlib3 documentation

measure_theory.group.pointwise

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) :
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) :
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) :
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₀) :