restrict_preimage_emb — Mathlib

English

If f is measure-preserving with a measurable embedding, restricting to s and preimage preserves the measure.

Русский

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

LaTeX

$$$hf: MeasurePreserving f μa μb \\wedge h₂: MeasurableEmbedding f \\Rightarrow \\forall s, MeasurePreserving f (μa.restrict (f^{-1} s)) (μb.restrict s)$$$

Lean4

theorem restrict_preimage_emb {f : α → β} (hf : MeasurePreserving f μa μb) (h₂ : MeasurableEmbedding f) (s : Set β) :
    MeasurePreserving f (μa.restrict (f ⁻¹' s)) (μb.restrict s) :=
  ⟨hf.measurable, by rw [← hf.map_eq, h₂.restrict_map]⟩

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