const_smul₀ — Mathlib

English

The map (x, y) ↦ (y, yx) preserves μ × ν when ν is left-invariant.

Русский

Отображение (x, y) ↦ (y, yx) сохраняет произведение мер μ × ν при условии, что ν — слева-инвариантна.

LaTeX

$$MeasurePreserving (fun z : G × G => (z.2, z.2 * z.1)) (μ.prod ν) (ν.prod μ)$$

Lean4

theorem const_smul₀ {G₀ α : Type*} [GroupWithZero G₀] [Zero α] [MulActionWithZero G₀ α] [MeasurableSpace G₀]
    [MeasurableSpace α] [MeasurableSMul G₀ α] [MeasurableSingletonClass α] {s : Set α} (hs : MeasurableSet s) (a : G₀) :
    MeasurableSet (a • s) := by
  rcases eq_or_ne a 0 with (rfl | ha)
  exacts [(subsingleton_zero_smul_set s).measurableSet, hs.const_smul_of_ne_zero ha]

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