English
There is a natural Smul action of DomMulAct M on the space of AEStronglyMeasurable functions modulo almost everywhere equality, defined by precomposition with the inverse action on the base space.
Русский
Существует естественное действие на пространстве классов почти всюду сильно измеримых функций, факторизованных по отношению почти равенства, которому соответствует предкомпозиция с обратным действием на базовом множесте.
LaTeX
$$$\\text{Smul} : DomMulAct(M) \\ times (\\alpha \\to_{μ} β) \\to (\\alpha \\to_{μ} β)$, задаваемое $c \\cdot f := f \\circ (c^{-1} \\cdot -)$ на представителях, устойчива относительно эквивалентности а.е.$$
Lean4
@[to_additive]
instance : SMul Mᵈᵐᵃ (α →ₘ[μ] β) where smul c f := f.compMeasurePreserving (mk.symm c • ·) (measurePreserving_smul _ _)
