measure_smul — Mathlib

English

If a map f preserves μ, then μ is invariant under the action generated by iterates of f; i.e., for every n ∈ N and every measurable set S, μ((f^n)⁻¹(S)) = μ(S).

Русский

Если отображение f сохраняет меру μ, то μ инвариантно относительно действия, генерируемого повторениями f; то есть для любого естественного n и любо́го измеримого множества S выполняется μ((f^n)⁻¹(S)) = μ(S).

LaTeX

$$$\\forall n \\in \\mathbb{N}, \\forall S,\\ \\text{Measurable}(S) \\Rightarrow \\mu\\big((f^n)^{-1}(S)\\big) = \\mu(S)$$$

Lean4

@[to_additive (attr := simp)]
theorem measure_smul (c : G) (s : Set α) : μ (c • s) = μ s := by
  simpa only [preimage_smul_inv] using measure_preimage_smul μ c⁻¹ s

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