map_apply — Mathlib

English

There is a compatibility between pushing forward a measure and pushing forward its outer measure: toOuterMeasure of μ.map f equals the trimmed outer map of μ.toOuterMeasure.

Русский

Сопоставимость образа меры и её внешней меры: toOuterMeasure(μ.map f) = OuterMeasure.map f (toOuterMeasure μ) с усечением.

LaTeX

$$$ (\mu.map f).toOuterMeasure = (OuterMeasure.map f \mu.toOuterMeasure).trim $ for AEMeasurable f μ$$

Lean4

@[simp]
theorem map_apply (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) : μ.map f s = μ (f ⁻¹' s) :=
  map_apply_of_aemeasurable hf.aemeasurable hs

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