measurePreserving_smul — Mathlib

English

For a fixed c ∈ M, the map x ↦ c • x is measure-preserving: μ preserves the measure under smul by c.

Русский

Пусть c ∈ M; отображение x ↦ c • x сохраняет меру: мерa μ сохраняется при смуле на c.

LaTeX

$$$\\text{MeasurePreserving}(c\\cdot,\\mu,\\mu)$$$

Lean4

@[to_additive (attr := simp)]
theorem measurePreserving_smul : MeasurePreserving (c • ·) μ μ :=
  { measurable := measurable_const_smul c
    map_eq := by
      ext1 s hs
      rw [map_apply (measurable_const_smul c) hs]
      exact SMulInvariantMeasure.measure_preimage_smul c hs }

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