le_map_apply — Mathlib

English

For AEMeasurable f, and any set s, μ(f^{-1}(s)) ≤ (μ.map f)(s).

Русский

Для AEMeasurable f и любого множества s выполняется неравенство μ(f^{-1}(s)) ≤ (μ.map f)(s).

LaTeX

$$$ \mu (f^{-1}(s)) \le (\mu.map f)(s) $$$

Lean4

/-- Even if `s` is not measurable, we can bound `map f μ s` from below.
  See also `MeasurableEquiv.map_apply`. -/
theorem le_map_apply {f : α → β} (hf : AEMeasurable f μ) (s : Set β) : μ (f ⁻¹' s) ≤ μ.map f s :=
  calc
    μ (f ⁻¹' s) ≤ μ (f ⁻¹' toMeasurable (μ.map f) s) := by gcongr; apply subset_toMeasurable
    _ = μ.map f (toMeasurable (μ.map f) s) := (map_apply_of_aemeasurable hf <| measurableSet_toMeasurable _ _).symm
    _ = μ.map f s := measure_toMeasurable _

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