measure_preimage_emb — Mathlib

English

If f preserves μa to μb and f is a measurable embedding, then μa(f^{-1}(s)) = μb(s) for all s.

Русский

Если f сохраняет μа→μb и является измеримо вложением, то для всякого s выполняется μa(f^{-1}(s)) = μb(s).

LaTeX

$$$\text{MeasurePreserving } f\, μ_a\, μ_b \rightarrow \text{MeasurableEmbedding } f \rightarrow \forall s, μ_a(f^{-1}(s)) = μ_b(s)$$$

Lean4

theorem measure_preimage_emb {f : α → β} (hf : MeasurePreserving f μa μb) (hfe : MeasurableEmbedding f) (s : Set β) :
    μa (f ⁻¹' s) = μb s := by rw [← hf.map_eq, hfe.map_apply]

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