measure_mem_eq — Mathlib

English

If h is IdentDistrib f g μ ν then for any measurable s, preimages under f and g have equal measure.

Русский

Если h — IdentDistrib f g μ ν, то для любого измеримого множества s множества-образ f и g имеют равные меры.

LaTeX

$$$h :\ IdentDistrib f g μ ν \to\ \forall s\ MeasurableSet s, μ(f^{-1}(s)) = ν(g^{-1}(s))$$$

Lean4

theorem measure_mem_eq (h : IdentDistrib f g μ ν) {s : Set γ} (hs : MeasurableSet s) : μ (f ⁻¹' s) = ν (g ⁻¹' s) := by
  rw [← Measure.map_apply_of_aemeasurable h.aemeasurable_fst hs, ←
    Measure.map_apply_of_aemeasurable h.aemeasurable_snd hs, h.map_eq]

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