const_smul — Mathlib

English

If s is a measurable set in α and a is a group element acting by scaling, then a • s is measurable.

Русский

Если s — измеримое множество в α, и a действует на α умножением/скалированием, то a • s измеримо.

LaTeX

$$MeasurableSet(a \\cdot s)$$

Lean4

@[to_additive]
theorem const_smul {G α : Type*} [Group G] [MulAction G α] [MeasurableSpace G] [MeasurableSpace α] [MeasurableSMul G α]
    {s : Set α} (hs : MeasurableSet s) (a : G) : MeasurableSet (a • s) :=
  by
  rw [← preimage_smul_inv]
  exact measurable_const_smul _ hs

Похожие утверждения