feat(topology/algebra/module/weak_dual): weak_space is functorial (#…

…16441)

src/topology/algebra/module/weak_dual.lean

@@ -248,6 +248,22 @@ def weak_space (𝕜 E) [comm_semiring 𝕜] [topological_space 𝕜] [has_conti
   [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] :=
 weak_bilin (top_dual_pairing 𝕜 E).flip
 
+namespace weak_space
+
+variables {𝕜 E F} [add_comm_monoid F] [module 𝕜 F] [topological_space F]
+
+/-- 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) :
+  weak_space 𝕜 E →L[𝕜] weak_space 𝕜 F :=
+{ cont := weak_bilin.continuous_of_continuous_eval _ (λ l, weak_bilin.eval_continuous _ (l ∘L f)),
+  ..f }
+
+lemma map_apply (f : E →L[𝕜] F) (x : E) : weak_space.map f x = f x := rfl
+@[simp] lemma coe_map (f : E →L[𝕜] F) : (weak_space.map f : E → F) = f := rfl
+
+end weak_space
+
 theorem tendsto_iff_forall_eval_tendsto_top_dual_pairing
   {l : filter α} {f : α → weak_dual 𝕜 E} {x : weak_dual 𝕜 E} :
   tendsto f l (𝓝 x) ↔