measure_preimage_inv — Mathlib

English

If μ is inv-invariant, then for every measurable A, μ( inv⁻¹(A) ) = μ(A).

Русский

Если μ инвариантна относительно инверсии, то для каждого измеримого множества A выполняется μ( inv⁻¹(A) ) = μ(A).

LaTeX

$$$ \mu(\mathrm{inv}^{-1}(A)) = \mu(A) $$$

Lean4

@[to_additive]
theorem measure_preimage_inv (μ : Measure G) [IsInvInvariant μ] (A : Set G) : μ (Inv.inv ⁻¹' A) = μ A :=
  μ.measure_inv A

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