mul_right — Mathlib

English

The lemma states that if f is measure-preserving from μ' to μ, then x ↦ f(x) g is measure-preserving from μ' to μ.

Русский

Лемма говорит, что если f сохраняет меру, то x ↦ f(x) g сохраняет меру.

LaTeX

$$$\\text{MeasurePreserving}(f) \\Rightarrow \\text{MeasurePreserving}(x \\mapsto f(x) g)$$$

Lean4

@[to_additive]
theorem mul_right (μ : Measure G) [IsMulRightInvariant μ] (g : G) {X : Type*} [MeasurableSpace X] {μ' : Measure X}
    {f : X → G} (hf : MeasurePreserving f μ' μ) : MeasurePreserving (fun x => f x * g) μ' μ :=
  (measurePreserving_mul_right μ g).comp hf

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