English
There is a multiplicative homomorphism from the monoid of continuous maps C(α, β) into the monoid of μ-almost everywhere measurable functions α →ₘ[μ] β, given by mapping f to f.toAEEqFun μ.
Русский
Существует моноид-гомоморфизм от моноида непрерывных отображений C(α,β) к моноиду эквивалентностей по μ функции α →ₘ[μ] β, отправляющего f в f.toAEEqFun μ.
LaTeX
$$$\text{toAEEqFunMulHom}: C(α,β) \to_* α \to_{μ} β$ with $f \mapsto f.toAEEqFun μ$ and $1 \mapsto 1$, $fg \mapsto f.toAEEqFun μ \cdot g.toAEEqFun μ$.$$
Lean4
/-- The `MulHom` from the group of continuous maps from `α` to `β` to the group of equivalence
classes of `μ`-almost-everywhere measurable functions. -/
@[to_additive /-- The `AddHom` from the group of continuous maps from `α` to `β` to the group of
equivalence classes of `μ`-almost-everywhere measurable functions. -/
]
def toAEEqFunMulHom : C(α, β) →* α →ₘ[μ] β
where
toFun := ContinuousMap.toAEEqFun μ
map_one' := rfl
map_mul' f g := AEEqFun.mk_mul_mk _ _ f.continuous.aestronglyMeasurable g.continuous.aestronglyMeasurable
