restrict_map — Mathlib

English

For a measurable equivalence e, restricting the pushforward of μ by e equals mapping the restricted μ by e.

Русский

Для измеримого эквивалента e ограничение образа меры μ через e равно отображению ограниченной меры μ через e.

LaTeX

$$$ (μ.map e).restrict s = (μ.restrict (e^{-1}(s))).map e $$$

Lean4

theorem _root_.MeasurableEquiv.restrict_map (e : α ≃ᵐ β) (μ : Measure α) (s : Set β) :
    (μ.map e).restrict s = (μ.restrict <| e ⁻¹' s).map e :=
  e.measurableEmbedding.restrict_map _ _

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