smulInvariantMeasure_map_smul — Mathlib

English

If μ is SMulInvariantMeasure on α and n acts on α via smul with N, then map (n • ·) μ is SMulInvariantMeasure on α.

Русский

Если μ инвариантна относительно действия M на α, и n действует на α через умножение, то map (n • ·) μ также инвариантна.

LaTeX

$$$\\text{SMulInvariantMeasure } M \\alpha (\\operatorname{map}(n\\cdot,\\mu))$$$

Lean4

@[to_additive]
instance smulInvariantMeasure_map_smul [SMul M α] [SMul N α] [SMulCommClass N M α] [MeasurableSMul M α]
    [MeasurableSMul N α] (μ : Measure α) [SMulInvariantMeasure M α μ] (n : N) :
    SMulInvariantMeasure M α (map (n • ·) μ) :=
  smulInvariantMeasure_map μ _ (smul_comm n) <| measurable_const_smul _

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