English
A linear map f: E →L[𝕜] F induces a canonical continuous linear map between the corresponding weak spaces.
Русский
Линейное отображение f: E →L[𝕜] F порождает каноничное непрерывное линейное отображение между соответствующими слабопредставлениями.
LaTeX
$$$\\text{WeakSpace\\_map}(f)\\in\\mathrm{ContinuousLinearMap} (\\mathrm{WeakSpace } 𝕜 E, \\mathrm{WeakSpace } 𝕜 F)$$$
Lean4
/-- A continuous linear map from `E` to `F` is still continuous when `E` and `F` are equipped with
their weak topologies. -/
def map (f : E →L[𝕜] F) : WeakSpace 𝕜 E →L[𝕜] WeakSpace 𝕜 F :=
{ f with cont := WeakBilin.continuous_of_continuous_eval _ fun l => WeakBilin.eval_continuous _ (l ∘L f) }
