coeFn_compMeasurePreserving — Mathlib

English

The composition with a measure-preserving map is ae-equal to the pointwise composition.

Русский

Композиция с мероподдерживающим отображением эквивалентна по ae-пу к точной композиции.

LaTeX

$$$g.compMeasurePreserving f hf =ᵐ[\\mu] g \\circ f$$$

Lean4

theorem coeFn_compMeasurePreserving (g : β →ₘ[ν] γ) (hf : MeasurePreserving f μ ν) :
    g.compMeasurePreserving f hf =ᵐ[μ] g ∘ f :=
  g.coeFn_compQuasiMeasurePreserving _

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