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)