compMeasurePreserving — Mathlib

English

Composition with a measure-preserving map defines a new AE-equal function.

Русский

Композиция с меропродержащим отображением определяет новую AEEqFun.

LaTeX

$$$\\mathrm{compMeasurePreserving}(g,f,hf) = g.compQuasiMeasurePreserving f hf.quasiMeasurePreserving$$$

Lean4

/-- Composition of an almost everywhere equal function and a quasi-measure-preserving function.

This is an important special case of `AEEqFun.compQuasiMeasurePreserving`. We use a separate
definition so that lemmas that need `f` to be measure preserving can be `@[simp]` lemmas. -/
def compMeasurePreserving (g : β →ₘ[ν] γ) (f : α → β) (hf : MeasurePreserving f μ ν) : α →ₘ[μ] γ :=
  g.compQuasiMeasurePreserving f hf.quasiMeasurePreserving

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