measurableEmbedding_const_smul
theorem measurableEmbedding_const_smul :
∀ {G : Type u_1} {α : Type u_3} [inst : MeasurableSpace G] [inst_1 : MeasurableSpace α] [inst_2 : Group G]
[inst_3 : MulAction G α] [inst : MeasurableSMul G α] (c : G), MeasurableEmbedding fun x => c • x
This theorem states that for any given type `G`, and a type `α`, with `G` being a group that acts on `α` via multiplication (`MulAction G α`), assuming that `G` and `α` are measurable spaces and the operation of `G` on `α` is also measurable (`MeasurableSMul G α`), then for any constant `c` of type `G`, the function that maps each element `x` from `α` to the result of `c • x` is a measurable embedding. In other words, scalar multiplication by a constant in a measurable space is a measurable embedding.
More concisely: For any measurable group action `MulAction G α` and constant `c` in the measurable group `G`, the function `x ↦ c • x` is a measurable embedding from `α` to `α`.
|
measurableEmbedding_const_vadd
theorem measurableEmbedding_const_vadd :
∀ {G : Type u_1} {α : Type u_3} [inst : MeasurableSpace G] [inst_1 : MeasurableSpace α] [inst_2 : AddGroup G]
[inst_3 : AddAction G α] [inst : MeasurableVAdd G α] (c : G), MeasurableEmbedding fun x => c +ᵥ x
This theorem states that for any given type `G`, type `α`, and a constant `c` of type `G`, if `G` has a measurable space structure, `α` has a measurable space structure, `G` is an additive group, `G` acts on `α` additively, and this action is measurable, then the function that maps `x` to `c` added to `x` (`c +ᵥ x`) is a measurable embedding. A measurable embedding is a function that is both measurable and injective, and the preimage of any measurable set under this function is also measurable. The types `G` and `α` could be any types, such as real numbers, integers, etc., as long as the required structures are defined for them.
More concisely: If `G` is a measurable additive group acting measurably and additively on a measurable type `α`, then the function `x ↦ c + x` is a measurable embedding.
|