map_comap — Mathlib

English

The map of μ by Subtype.val along with comap Subtype.val recovers the restricted measure on s.

Русский

Преобразование меры μ через Subtype.val вместе с comap Subtype.val восстанавливает ограниченную меру на s.

LaTeX

$$$\mathrm{map}\; \mathrm{Subtype.val} \, (\mathrm{comap}\; \mathrm{Subtype.val}\; μ) = μ\;\text{restricted to } s$$$

Lean4

theorem map_comap (μ : Measure β) : (comap f μ).map f = μ.restrict (range f) :=
  by
  ext1 t ht
  rw [hf.map_apply, comap_apply f hf.injective hf.measurableSet_image' _ (hf.measurable ht),
    image_preimage_eq_inter_range, Measure.restrict_apply ht]

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