map_apply' — Mathlib

English

Push-forward satisfies (ν.map f)(A) = ν(f^{-1}(A)) for ν a finite measure, with f measurable and A measurable.

Русский

Пересылка меры по измеримой функции удовлетворяет (ν.map f)(A) = ν(f^{-1}(A)).

LaTeX

$$$\\nu.map f(A) = \\nu(f^{-1}(A))$ for all measurable A when f is measurable$$

Lean4

/-- Note that this is an equality of elements of `ℝ≥0∞`. See also
`MeasureTheory.FiniteMeasure.map_apply` for the corresponding equality as elements of `ℝ≥0`. -/
theorem map_apply' (ν : FiniteMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ν) {A : Set Ω'}
    (A_mble : MeasurableSet A) : (ν.map f : Measure Ω') A = (ν : Measure Ω) (f ⁻¹' A) :=
  Measure.map_apply_of_aemeasurable f_aemble A_mble

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