measurePreserving_symm — Mathlib

English

If e is a measurable equivalence between α and β, then the pushforward of μ by e preserves μ when reversed by e, i.e., e.symm preserves map(e, μ) to μ.

Русский

Если e — измеримая эквивалентность между α и β, то возмещение μ по e сохраняется назад через e.symm.

LaTeX

$$$\forall μ\, e: α \toβ\,\; \text{MeasurePreserving } e^{\!-1} ( \text{map } e μ) μ$$$

Lean4

theorem measurePreserving_symm (μ : Measure α) (e : α ≃ᵐ β) : MeasurePreserving e.symm (map e μ) μ :=
  (e.measurable.measurePreserving μ).symm _

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