map_apply — Mathlib

English

If f is a MeasurableEquiv between α and β, then for every set s, μ.map f s = μ(f^{-1}(s)).

Русский

Если f — измеримое эквивалентное отображение между α и β, то для любого множества s верно μ.map f s = μ(f^{-1}(s)).

LaTeX

$$$$\\forall f:\\alpha \\to \\beta,\\; \\text{MeasurableEquiv}(f)\\rightarrow \\forall \\mu:\\mathrm{Measure}\\,\\alpha,\\forall s:\\mathrm Set_{\\beta},\\; \\mu.map f\\,s = \\mu\\,(f^{-1} s).$$$$

Lean4

/-- If we map a measure along a measurable equivalence, we can compute the measure on all sets
  (not just the measurable ones). -/
protected theorem map_apply (f : α ≃ᵐ β) (s : Set β) : μ.map f s = μ (f ⁻¹' s) :=
  f.measurableEmbedding.map_apply _ _

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