English
Let f: α → β be a function, and let μ be a measure on α. If a fixed element c of G acts on β by a measurable action, then left-multiplication by c preserves almost everywhere measurability: AEMeasurable (x ↦ c • f(x)) μ is equivalent to AEMeasurable f μ.
Русский
Пусть f: α → β и μ — мера на α. Пусть фиксированное элемент c из G действует на β посредством измеримого действия. Тогда левая операция умножения на c сохраняет почти всюкую измеримость: AEMeasurable (λx, c • f(x)) μ эквивалентно AEMeasurable f μ.
LaTeX
$$$AEMeasurable (\\lambda x. c \\cdot f(x))\\mu \\iff AEMeasurable f\\mu$$$
Lean4
@[to_additive]
theorem aemeasurable_const_smul_iff (c : G) : AEMeasurable (fun x => c • f x) μ ↔ AEMeasurable f μ :=
⟨fun h => by simpa [inv_smul_smul, Pi.smul_def] using h.const_smul c⁻¹, fun h => h.const_smul c⟩
