coeFn_compQuasiMeasurePreserving — Mathlib

English

The a.e.-equality of the composed function with the pointwise composition holds.

Русский

Ae-equality композиции и точной композиции выполняется.

LaTeX

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

Lean4

theorem coeFn_compQuasiMeasurePreserving (g : β →ₘ[ν] γ) (hf : QuasiMeasurePreserving f μ ν) :
    g.compQuasiMeasurePreserving f hf =ᵐ[μ] g ∘ f :=
  by
  rw [compQuasiMeasurePreserving_eq_mk]
  apply coeFn_mk

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