# mathlibdocumentation

measure_theory.group.pointwise

# Pointwise set operations on measurable_sets #

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] [ α] [ α] {s : set α} (hs : measurable_set s) (a : G) :
theorem measurable_set.const_vadd {G : Type u_1} {α : Type u_2} [add_group 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₀] [ α] [measurable_space 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 α] [ α] [measurable_space G₀] [ α] {s : set α} (hs : measurable_set s) (a : G₀) :