compQuasiMeasurePreserving_eq_mk — Mathlib

English

Equality of the quasinormalized composition with mk of the composition.

Русский

Равенство композиции через mk и через функцию композиции.

LaTeX

$$$g.compQuasiMeasurePreserving f hf = mk (g \\circ f) (g.aestronglyMeasurable.comp_quasiMeasurePreserving hf)$$$

Lean4

theorem compQuasiMeasurePreserving_eq_mk (g : β →ₘ[ν] γ) (hf : QuasiMeasurePreserving f μ ν) :
    g.compQuasiMeasurePreserving f hf = mk (g ∘ f) (g.aestronglyMeasurable.comp_quasiMeasurePreserving hf) := by
  rw [← compQuasiMeasurePreserving_mk g.aestronglyMeasurable hf, mk_coeFn]

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