trim_comap_apply — Mathlib

English

For a measurable f, and measurable s, μ.trim hm (f^{-1}(s)) = μ.map f (s).

Русский

Для измеримого f и измеримого s выполняется μ.trim hm (f^{-1}(s)) = μ.map f (s).

LaTeX

$$$μ.trim hm (f^{-1}(s)) = μ.map f (s).$$$

Lean4

theorem trim_comap_apply {f : α → β} (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) :
    μ.trim hf.comap_le (f ⁻¹' s) = μ.map f s := by
  rw [← map_trim_comap hf, Measure.map_apply (Measurable.of_comap_le le_rfl) hs]

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