English
Pre-composition by a fixed continuous linear map L yields a continuous linear map from F →SL[τ] G to E →SL[ρ] G, i.e., f ↦ f ∘ L defines a continuous linear operation.
Русский
Предпосложение по фиксированному пределу непрерывных линейных отображений L даёт непрерывный линейный отображатель, который отправляет f ∈ F →SL[τ] G в f ∘ L ∈ E →SL[ρ] G.
LaTeX
$$$\ntoLinearMap_{12} (L) : (F \\toSL[τ] G) →SL[𝕜_3] E →SL[ρ] G,\\n\\toFun f := f \\circ L$$$
Lean4
/-- Pre-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 precomp [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [RingHomSurjective σ] [RingHomIsometric σ]
(L : E →SL[σ] F) : (F →SL[τ] G) →L[𝕜₃] E →SL[ρ] G
where
toFun f := f.comp L
map_add' f g := add_comp f g L
map_smul' a f := smul_comp a f L
cont := by
letI : UniformSpace G := IsTopologicalAddGroup.toUniformSpace G
haveI : IsUniformAddGroup G := isUniformAddGroup_of_addCommGroup
rw [(UniformConvergenceCLM.isEmbedding_coeFn _ _ _).continuous_iff]
apply
(UniformOnFun.precomp_uniformContinuous fun S hS => hS.image L).continuous.comp
(UniformConvergenceCLM.isEmbedding_coeFn _ _ _).continuous
