English
There is a κ-linear map from the vector space of continuous maps C(α, γ) to the AEEqFun α γ μ, i.e., the map f ↦ f.toAEEqFun μ is κ-linear with respect to the scalar field κ.
Русский
Существуют κ-линейные отображения от пространства непрерывных отображений C(α, γ) в AEEqFun α γ μ, т.е. отображение f ↦ f.toAEEqFun μ линейно по скалярам κ.
LaTeX
$$$\text{toAEEqFunLinearMap}: C(α, γ) \to_{ℓ} α →ₘ[μ] γ$ является κ-линейным отображением.$$
Lean4
/-- The linear map from the group of continuous maps from `α` to `β` to the group of equivalence
classes of `μ`-almost-everywhere measurable functions. -/
def toAEEqFunLinearMap : C(α, γ) →ₗ[𝕜] α →ₘ[μ] γ :=
{ toAEEqFunAddHom μ with map_smul' := fun c f => AEEqFun.smul_mk c f f.continuous.aestronglyMeasurable }
