English
Post-composition by a fixed continuous linear map L yields a continuous linear map from E →SL[σ] F to E →SL[ρ] G, i.e., f ↦ L ∘ f is continuous linear in the appropriate sense.
Русский
Посткомпозиция по фиксированному отображению L даёт непрерывное линейное отображение из E →SL[σ] F в E →SL[ρ] G, т.е. f ↦ L ∘ f непрерывна и линейна.
LaTeX
$$$\nPostcomp_L : (E \\toSL[σ] F) →SL[τ] E →SL[ρ] G,\\nPostcomp_L(f) = L \\circ f$$$
Lean4
/-- Post-composition by a *fixed* continuous linear map as a continuous linear map.
Note that in non-normed space it is not always true that composition is continuous
in both variables, so we have to fix one of them. -/
@[simps]
def postcomp [IsTopologicalAddGroup F] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₂ F]
(L : F →SL[τ] G) : (E →SL[σ] F) →SL[τ] E →SL[ρ] G
where
toFun f := L.comp f
map_add' := comp_add L
map_smul' := comp_smulₛₗ L
cont := by
letI : UniformSpace G := IsTopologicalAddGroup.toUniformSpace G
haveI : IsUniformAddGroup G := isUniformAddGroup_of_addCommGroup
letI : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
rw [(UniformConvergenceCLM.isEmbedding_coeFn _ _ _).continuous_iff]
exact
(UniformOnFun.postcomp_uniformContinuous L.uniformContinuous).continuous.comp
(UniformConvergenceCLM.isEmbedding_coeFn _ _ _).continuous
