measure_preimage_smul — Mathlib

English

Let μ be a measure on α that is invariant under the action of a group G. Then for every c in G and every subset s of α, the measure of the preimage of s under the map x ↦ c · x is equal to μ(s).

Русский

Пусть μ — мера на α, инвариантная относительно действия группы G. Тогда для любого элемента c ∈ G и любого подмножества s ⊆ α выполняется μ((c · · )⁻¹ s) = μ(s).

LaTeX

$$$ \\mu\\big((c \\cdot \\cdot)^{-1}(s)\\big) = \\mu(s)$$$

Lean4

@[to_additive (attr := simp)]
theorem measure_preimage_smul (c : G) (s : Set α) : μ ((c • ·) ⁻¹' s) = μ s :=
  (measure_preimage_smul_le μ c s).antisymm <| by
    simpa [preimage_preimage] using measure_preimage_smul_le μ c⁻¹ ((c • ·) ⁻¹' s)

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