feat(Topology/Algebra/Module/WeakDual): prove basic relations between the weak topology and the original topology (#11566)

(This PR continues #11472)
Prove the following basic facts about the weak topology in a topological vector space (or AddCommMonoid) `E`.
- any set that is open in the weak topology is open in the original topology.
- any function in `E` that converges to a point in the original topology (with respect to some filter) converges also in the weak topology.
- if a function in `E` converges to a point in the original topology, then its composition with a continuous linear functional converges.
- any function from `E` that is continuous in the weak topology is also continuous in the original topology.

Motivation: WeakSpace has some basic properties, analogue of which are proved for WeakDual.

I have some doubts:
- in order to avoid typeclass instance problem, I had to add a type ascription `continuousLinearMapToWeakSpace : E →L[𝕜] WeakSpace 𝕜 E` when needed. Is this fine or is there a canonical way to avoid it? (I tried to add `variable (𝕜 E) in` before def/thm but it gave type mismatch in many places)
- I made two theorems about IsOpen, but not sure about the naming convention.


[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Author: yoh-tanimoto

Mathlib/Topology/Algebra/Module/WeakDual.lean

@@ -328,6 +328,39 @@ theorem coe_map (f : E →L[𝕜] F) : (WeakSpace.map f : E → F) = f :=
 
 end WeakSpace
 
+variable (𝕜 E) in
+/-- There is a canonical map `E → WeakSpace 𝕜 E` (the "identity"
+mapping). It is a linear equivalence. -/
+def toWeakSpace : E ≃ₗ[𝕜] WeakSpace 𝕜 E := LinearEquiv.refl 𝕜 E
+
+variable (𝕜 E) in
+/-- For a topological vector space `E`, "identity mapping" `E → WeakSpace 𝕜 E` is continuous.
+This definition implements it as a continuous linear map. -/
+def continuousLinearMapToWeakSpace : E →L[𝕜] WeakSpace 𝕜 E where
+  __ := toWeakSpace 𝕜 E
+  cont := by
+    apply WeakBilin.continuous_of_continuous_eval
+    exact ContinuousLinearMap.continuous
+
+variable (𝕜 E) in
+@[simp]
+theorem continuousLinearMapToWeakSpace_eq_toWeakSpace (x : E) :
+    continuousLinearMapToWeakSpace 𝕜 E x = toWeakSpace 𝕜 E x := by rfl
+
+theorem continuousLinearMapToWeakSpace_bijective :
+    Function.Bijective (continuousLinearMapToWeakSpace 𝕜 E) :=
+  (toWeakSpace 𝕜 E).bijective
+
+/-- The canonical map from `WeakSpace 𝕜 E` to `E` is an open map. -/
+theorem isOpenMap_toWeakSpace_symm : IsOpenMap (toWeakSpace 𝕜 E).symm :=
+  IsOpenMap.of_inverse (continuousLinearMapToWeakSpace 𝕜 E).cont
+    (toWeakSpace 𝕜 E).left_inv (toWeakSpace 𝕜 E).right_inv
+
+/-- A set in `E` which is open in the weak topology is open. -/
+theorem WeakSpace.isOpen_of_isOpen (V : Set E)
+    (hV : IsOpen ((continuousLinearMapToWeakSpace 𝕜 E) '' V : Set (WeakSpace 𝕜 E))) : IsOpen V := by
+  simpa [Set.image_image] using isOpenMap_toWeakSpace_symm _ hV
+
 theorem tendsto_iff_forall_eval_tendsto_topDualPairing {l : Filter α} {f : α → WeakDual 𝕜 E}
     {x : WeakDual 𝕜 E} :
     Tendsto f l (𝓝 x) ↔