English
Composition of a measurable g with an AE-equal f yields an AE-equal composite in the second target space.
Русский
Компоновка измеримой функции g с AEEqFun f образует AEEqFun-образец для γ.
LaTeX
$$$\\mathrm{compMeasurable}(g,hg,f) = \\mathrm{mk}(g \\circ f) (hg.comp_aemeasurable f.aemeasurable).aestronglyMeasurable$$$
Lean4
/-- Given a continuous function `g : β → γ`, and an almost everywhere equal function `[f] : α →ₘ β`,
return the equivalence class of `g ∘ f`, i.e., the almost everywhere equal function
`[g ∘ f] : α →ₘ γ`. -/
def comp (g : β → γ) (hg : Continuous g) (f : α →ₘ[μ] β) : α →ₘ[μ] γ :=
Quotient.liftOn' f (fun f => mk (g ∘ (f : α → β)) (hg.comp_aestronglyMeasurable f.2)) fun _ _ H =>
mk_eq_mk.2 <| H.fun_comp g
