compMeasurable_eq_mk — Mathlib

English

Equality of the mk-form of composed measurable function with the standard mk of the composition.

Русский

Равенство mk-формы композиции измеримой функции и mk композиции.

LaTeX

$$$\\mathrm{compMeasurable\\_eq\\_mk}(g,hg,f) = \\mathrm{mk}(g\\circ f)(hg\\circ f.aemeasurable).aestronglyMeasurable$$$

Lean4

theorem compMeasurable_eq_mk (g : β → γ) (hg : Measurable g) (f : α →ₘ[μ] β) :
    compMeasurable g hg f = mk (g ∘ f) (hg.comp_aemeasurable f.aemeasurable).aestronglyMeasurable := by
  rw [← compMeasurable_mk g hg f f.aestronglyMeasurable, mk_coeFn]

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