compMeasurePreserving_mk — Mathlib

English

The mk-construction of a composed function with measure-preserving f yields mk of the composition.

Русский

Конструкция mk для композиции через measure-preserving соответствует mk композиции.

LaTeX

$$$\\mathrm{compMeasurePreserving\\_mk}(hg,hf) = \\mathrm{mk}(g \\circ f) (hg.comp\\_quasiMeasurePreserving hf.quasiMeasurePreserving)$$$

Lean4

@[simp]
theorem compMeasurePreserving_mk (hg : AEStronglyMeasurable g ν) (hf : MeasurePreserving f μ ν) :
    (mk g hg).compMeasurePreserving f hf = mk (g ∘ f) (hg.comp_quasiMeasurePreserving hf.quasiMeasurePreserving) :=
  rfl

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