map_trim_comap — Mathlib

English

If f is measurable, then the pushforward of μ.trim by f with comap mβ equals the pushforward of μ by f with μ: map f (μ.trim) = map f μ.

Русский

Пусть f мерозмерна, тогда произведение отображения μ.trim по f эквивалентно μ по f: map f (μ.trim) = map f μ.

LaTeX

$$$\\operatorname{map} f (μ.trim) = μ.map f.$$$

Lean4

theorem map_trim_comap {f : α → β} (hf : Measurable f) :
    @Measure.map _ _ (mβ.comap f) _ f (μ.trim hf.comap_le) = μ.map f :=
  by
  ext s hs
  rw [Measure.map_apply hf hs, Measure.map_apply _ hs, trim_measurableSet_eq]
  · exact ⟨s, hs, rfl⟩
  · exact Measurable.of_comap_le le_rfl

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