compQuasiMeasurePreserving_mk — Mathlib

English

A simplification: the mk-constructed composition equals the mk of the composition.

Русский

Упрощение: композиция, сконструированная через mk, равна mk-композиции.

LaTeX

$$$(\\mathrm{mk}\ g\\ hf) .\\!\\text{compQuasiMeasurePreserving } f hf = \\mathrm{mk}(g \\circ f)(hg \\circ \\text{...})$$$

Lean4

@[simp]
theorem compQuasiMeasurePreserving_mk {g : β → γ} (hg : AEStronglyMeasurable g ν) (hf : QuasiMeasurePreserving f μ ν) :
    (mk g hg).compQuasiMeasurePreserving f hf = mk (g ∘ f) (hg.comp_quasiMeasurePreserving hf) :=
  rfl

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