restrict_image_emb — Mathlib

English

If f is measure-preserving with a measurable embedding, then restricting to s yields a measure-preserving map to f''s.

Русский

Если f сохраняет меру и является измеримо вложением, ограничение области к образу сохраняет меру.

LaTeX

$$$hf: MeasurePreserving f μa μb \\wedge h₂: MeasurableEmbedding f \\Rightarrow \\forall s, MeasurePreserving f (μa.restrict s) (μb.restrict (f '' s))$$$

Lean4

theorem restrict_image_emb {f : α → β} (hf : MeasurePreserving f μa μb) (h₂ : MeasurableEmbedding f) (s : Set α) :
    MeasurePreserving f (μa.restrict s) (μb.restrict (f '' s)) := by
  simpa only [Set.preimage_image_eq _ h₂.injective] using hf.restrict_preimage_emb h₂ (f '' s)

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