const_smul_of_ne_zero — Mathlib

English

If a ≠ 0 in a group-with-zero acting on α, then a • s is measurable whenever s is measurable.

Русский

Если a ≠ 0 в группе с нулём, действующей на α, то a • s измеримо при условии, что s измеримо.

LaTeX

$$MeasurableSet(a • s)$$

Lean4

theorem const_smul_of_ne_zero {G₀ α : Type*} [GroupWithZero G₀] [MulAction G₀ α] [MeasurableSpace G₀]
    [MeasurableSpace α] [MeasurableSMul G₀ α] {s : Set α} (hs : MeasurableSet s) {a : G₀} (ha : a ≠ 0) :
    MeasurableSet (a • s) := by
  rw [← preimage_smul_inv₀ ha]
  exact measurable_const_smul _ hs

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