diff --git a/Mathlib.lean b/Mathlib.lean
index 09a2198e928739..74f650fde894f2 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1963,7 +1963,7 @@ public import Mathlib.Analysis.LocallyConvex.Polar
 public import Mathlib.Analysis.LocallyConvex.SeparatingDual
 public import Mathlib.Analysis.LocallyConvex.Separation
 public import Mathlib.Analysis.LocallyConvex.StrongTopology
-public import Mathlib.Analysis.LocallyConvex.WeakDual
+public import Mathlib.Analysis.LocallyConvex.WeakBilin
 public import Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
 public import Mathlib.Analysis.LocallyConvex.WeakSpace
 public import Mathlib.Analysis.LocallyConvex.WithSeminorms
@@ -2097,6 +2097,7 @@ public import Mathlib.Analysis.Normed.Module.Shrink
 public import Mathlib.Analysis.Normed.Module.Span
 public import Mathlib.Analysis.Normed.Module.TransferInstance
 public import Mathlib.Analysis.Normed.Module.WeakDual
+public import Mathlib.Analysis.Normed.Module.WeakSpace
 public import Mathlib.Analysis.Normed.MulAction
 public import Mathlib.Analysis.Normed.Operator.Asymptotics
 public import Mathlib.Analysis.Normed.Operator.Banach
@@ -7240,6 +7241,7 @@ public import Mathlib.Topology.Algebra.Module.TransferInstance
 public import Mathlib.Topology.Algebra.Module.UniformConvergence
 public import Mathlib.Topology.Algebra.Module.WeakBilin
 public import Mathlib.Topology.Algebra.Module.WeakDual
+public import Mathlib.Topology.Algebra.Module.WeakSpace
 public import Mathlib.Topology.Algebra.Monoid
 public import Mathlib.Topology.Algebra.Monoid.AddChar
 public import Mathlib.Topology.Algebra.Monoid.Defs
diff --git a/Mathlib/Analysis/LocallyConvex/WeakDual.lean b/Mathlib/Analysis/LocallyConvex/WeakBilin.lean
similarity index 98%
rename from Mathlib/Analysis/LocallyConvex/WeakDual.lean
rename to Mathlib/Analysis/LocallyConvex/WeakBilin.lean
index f42be09aeb6c1f..e5dfa590ad0f20 100644
--- a/Mathlib/Analysis/LocallyConvex/WeakDual.lean
+++ b/Mathlib/Analysis/LocallyConvex/WeakBilin.lean
@@ -12,7 +12,7 @@ public import Mathlib.LinearAlgebra.Finsupp.Span
 public import Mathlib.Topology.Algebra.Module.WeakBilin
 
 /-!
-# Weak Dual in Topological Vector Spaces
+# Weak Bilinear Topologies in Topological Vector Spaces
 
 We prove that the weak topology induced by a bilinear form `B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜` is locally
 convex and we explicitly give a neighborhood basis in terms of the family of seminorms
@@ -28,7 +28,7 @@ convex and we explicitly give a neighborhood basis in terms of the family of sem
 
 * `LinearMap.hasBasis_weakBilin`: the seminorm balls of `B.toSeminormFamily` form a
   neighborhood basis of `0` in the weak topology.
-* `LinearMap.toSeminormFamily.withSeminorms`: the topology of a weak space is induced by the
+* `LinearMap.weakBilin_withSeminorms`: the topology of a weak space is induced by the
   family of seminorms `B.toSeminormFamily`.
 * `WeakBilin.locallyConvexSpace`: a space endowed with a weak topology is locally convex.
 * `LinearMap.rightDualEquiv`: When `B` is right-separating, `F` is linearly equivalent to the
@@ -43,7 +43,7 @@ convex and we explicitly give a neighborhood basis in terms of the family of sem
 
 ## Tags
 
-weak dual, seminorm
+weak bilinear, seminorm
 -/
 
 @[expose] public section
diff --git a/Mathlib/Analysis/LocallyConvex/WeakSpace.lean b/Mathlib/Analysis/LocallyConvex/WeakSpace.lean
index a20819b1f86a82..9d2afe956a9fe6 100644
--- a/Mathlib/Analysis/LocallyConvex/WeakSpace.lean
+++ b/Mathlib/Analysis/LocallyConvex/WeakSpace.lean
@@ -1,17 +1,26 @@
 /-
 Copyright (c) 2024 Jireh Loreaux. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jireh Loreaux
+Authors: Jireh Loreaux, Michał Świętek
 -/
 module
 
 public import Mathlib.Analysis.LocallyConvex.Separation
+public import Mathlib.Analysis.LocallyConvex.WeakBilin
 public import Mathlib.LinearAlgebra.Dual.Defs
-public import Mathlib.Topology.Algebra.Module.WeakDual
+public import Mathlib.Topology.Algebra.Module.WeakSpace
 
-/-! # Closures of convex sets in locally convex spaces
+/-! # Weak topology on normed spaces: seminorm family and convex closures
 
-This file contains the standard result that if `E` is a vector space with two locally convex
+## Seminorm family
+
+The weak topology on `WeakSpace 𝕜 E` is generated by the seminorm family `fun f x ↦ ‖f x‖`
+indexed by `StrongDual 𝕜 E`. This follows from the general `LinearMap.weakBilin_withSeminorms`
+applied to the flipped `topDualPairing`.
+
+## Closures of convex sets
+
+This file also contains the standard result that if `E` is a vector space with two locally convex
 topologies, then the closure of a convex set is the same in either topology, provided they have the
 same collection of continuous linear functionals. In particular, the weak closure of a convex set
 in a locally convex space coincides with the closure in the original topology.
@@ -19,7 +28,38 @@ Of course, we phrase this in terms of linear maps between locally convex spaces,
 creating two separate topologies on the same space.
 -/
 
-public section
+@[expose] public section
+
+section Seminorms
+
+variable {𝕜 : Type*} [NormedField 𝕜] {E : Type*} [AddCommGroup E] [Module 𝕜 E]
+  [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E]
+
+namespace WeakSpace
+
+set_option backward.isDefEq.respectTransparency false in
+variable (𝕜 E) in
+/-- The family of seminorms on `WeakSpace 𝕜 E` given by `fun f x ↦ ‖f x‖`, indexed by
+`StrongDual 𝕜 E`. This is the seminorm family associated to the weak topology via the
+flipped `topDualPairing`. -/
+def seminormFamily : SeminormFamily 𝕜 (WeakSpace 𝕜 E) (StrongDual 𝕜 E) :=
+  (topDualPairing 𝕜 E).flip.toSeminormFamily
+
+set_option backward.isDefEq.respectTransparency false in
+omit [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] in
+@[simp]
+lemma seminormFamily_apply (f : StrongDual 𝕜 E) (x : WeakSpace 𝕜 E) :
+    seminormFamily 𝕜 E f x = ‖f x‖ := rfl
+
+set_option backward.isDefEq.respectTransparency false in
+omit [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] in
+variable (𝕜 E) in
+lemma withSeminorms : WithSeminorms (seminormFamily 𝕜 E) :=
+  (topDualPairing 𝕜 E).flip.weakBilin_withSeminorms
+
+end WeakSpace
+
+end Seminorms
 
 variable {𝕜 E F : Type*}
 variable [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F]
diff --git a/Mathlib/Analysis/Normed/Module/WeakSpace.lean b/Mathlib/Analysis/Normed/Module/WeakSpace.lean
new file mode 100644
index 00000000000000..2506aa96a0061f
--- /dev/null
+++ b/Mathlib/Analysis/Normed/Module/WeakSpace.lean
@@ -0,0 +1,129 @@
+/-
+Copyright (c) 2026 Michał Świętek. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michał Świętek
+-/
+module
+
+public import Mathlib.Analysis.Normed.Module.HahnBanach
+public import Mathlib.Analysis.Normed.Module.WeakDual
+public import Mathlib.Analysis.LocallyConvex.WeakSpace
+import Mathlib.Analysis.Normed.Operator.BanachSteinhaus
+
+/-!
+# Normed space instances for `WeakSpace`
+
+This file provides basic instances for `WeakSpace 𝕜 E` in the setting of normed spaces.
+
+The file equips `WeakSpace 𝕜 E` with the norm bornology inherited from `E`, so that `IsBounded`
+refers to norm boundedness. This is a pragmatic choice discussed further in the implementation
+notes.
+
+## Main definitions
+
+* `WeakSpace.instBornology`: The norm bornology on `WeakSpace 𝕜 E`, inherited from `E`.
+* `WeakSpace.seminormFamily`: The family of seminorms `fun f x ↦ ‖f x‖` generating the weak
+  topology, indexed by `StrongDual 𝕜 E`.
+* `WeakSpace.instT2Space`: The weak topology on a normed space over `RCLike` is Hausdorff,
+  via Hahn–Banach separation.
+
+## Main results
+
+### Topology comparison
+* `WeakSpace.norm_topology_le_weakSpace_topology`: The weak topology is coarser than the norm
+  topology.
+
+### Bornology and pointwise bounds
+* `WeakSpace.isBounded_iff_isVonNBounded`: Equivalence of norm and weak boundedness for
+  normed spaces over `RCLike`.
+
+## Implementation notes
+
+* **Bornology choice:** The `Bornology` instance on `WeakSpace 𝕜 E` is inherited from `E` via
+  `inferInstanceAs` and corresponds to the norm bornology. While the natural bornology for a
+  weak topology is technically the von Neumann bornology (pointwise boundedness), we use the
+  norm bornology for several pragmatic reasons:
+  1. **Practicality:** In the normed setting, "bounded" is almost universally synonymous with
+     "norm-bounded". This allows `IsBounded` to be used directly.
+  2. **Clarity:** It preserves a clear distinction between norm-boundedness (`IsBounded`) and
+     topological weak boundedness (`IsVonNBounded`).
+  3. **Consistency:** By the Uniform Boundedness Principle, these notions coincide whenever
+     `𝕜` is `RCLike` (`isBounded_iff_isVonNBounded`). No `[CompleteSpace E]` assumption is
+     needed because `banach_steinhaus` is applied to the inclusion in the double dual, whose
+     domain `StrongDual 𝕜 E` is always complete when `𝕜` is `RCLike`.
+-/
+
+@[expose] public section
+
+noncomputable section
+
+open Bornology Topology
+
+namespace WeakSpace
+
+section NontriviallyNormedField
+
+variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
+variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
+
+/-- The norm bornology on `WeakSpace 𝕜 E`, inherited from `E`. -/
+instance instBornology : Bornology (WeakSpace 𝕜 E) := inferInstanceAs (Bornology E)
+
+/-- A set in `WeakSpace 𝕜 E` is bounded iff its image in `E` is bounded. -/
+@[simp]
+theorem isBounded_toE_preimage {s : Set E} :
+    IsBounded (⇑(toWeakSpace 𝕜 E).symm ⁻¹' s) ↔ IsBounded s :=
+  Iff.rfl
+
+/-- A set in `E` is bounded iff its image in `WeakSpace 𝕜 E` is bounded. -/
+@[simp]
+theorem isBounded_toWeakSpace_preimage {s : Set (WeakSpace 𝕜 E)} :
+    IsBounded (⇑(toWeakSpace 𝕜 E) ⁻¹' s) ↔ IsBounded s :=
+  Iff.rfl
+
+/-- The weak topology on a normed space is coarser than the norm topology. -/
+theorem norm_topology_le_weakSpace_topology :
+    (UniformSpace.toTopologicalSpace : TopologicalSpace E) ≤
+      (inferInstance : TopologicalSpace (WeakSpace 𝕜 E)) := by
+  convert (toWeakSpaceCLM 𝕜 E).continuous.le_induced
+  exact induced_id.symm
+
+end NontriviallyNormedField
+
+section RCLike
+
+variable (𝕜 : Type*) [RCLike 𝕜]
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+
+/-- The weak topology on a normed space over `RCLike` is T2 (Hausdorff). This follows from
+Hahn–Banach: the continuous linear functionals separate points. -/
+instance instT2Space : T2Space (WeakSpace 𝕜 E) :=
+  (WeakBilin.isEmbedding (B := (topDualPairing 𝕜 E).flip) fun x y h => by
+    obtain ⟨g, _, hg⟩ := exists_dual_vector'' 𝕜 (x - y)
+    rw [map_sub, show g x = g y from LinearMap.ext_iff.mp h g, sub_self] at hg
+    exact sub_eq_zero.mp (norm_eq_zero.mp (by exact_mod_cast hg.symm))).t2Space
+
+set_option backward.isDefEq.respectTransparency false in
+/-- By the Uniform Boundedness Principle, norm-boundedness (the default bornology)
+and pointwise-boundedness (`IsVonNBounded`) coincide on the weak space of a normed space
+over `RCLike`. -/
+theorem isBounded_iff_isVonNBounded {s : Set (WeakSpace 𝕜 E)} :
+    IsBounded s ↔ Bornology.IsVonNBounded 𝕜 s := by
+  constructor
+  · exact fun h => ((NormedSpace.isVonNBounded_iff (E := E) (𝕜 := 𝕜)).mpr h).of_topologicalSpace_le
+      norm_topology_le_weakSpace_topology
+  · intro h_vN
+    have h_ptwise := (WeakSpace.withSeminorms 𝕜 E).isVonNBounded_iff_seminorm_bounded.mp h_vN
+    obtain ⟨C, hC⟩ := banach_steinhaus
+      (g := fun i : s ↦ NormedSpace.inclusionInDoubleDual 𝕜 E i.val) fun f ↦
+      let ⟨M, _, hM⟩ := h_ptwise f
+      ⟨M, fun i ↦ le_of_lt (hM i.val i.property)⟩
+    suffices @IsBounded E _ s from this
+    rw [isBounded_iff_forall_norm_le]
+    exact ⟨C, fun x hx ↦ by
+      rw [← (NormedSpace.inclusionInDoubleDualLi 𝕜).norm_map x]
+      exact hC ⟨x, hx⟩⟩
+
+end RCLike
+
+end WeakSpace
diff --git a/Mathlib/Topology/Algebra/Module/WeakDual.lean b/Mathlib/Topology/Algebra/Module/WeakDual.lean
index 9188ee7caf0b2d..f31c0f8c6a7153 100644
--- a/Mathlib/Topology/Algebra/Module/WeakDual.lean
+++ b/Mathlib/Topology/Algebra/Module/WeakDual.lean
@@ -8,32 +8,20 @@ module
 public import Mathlib.LinearAlgebra.BilinearMap
 public import Mathlib.Topology.Algebra.Module.LinearMap
 public import Mathlib.Topology.Algebra.Module.WeakBilin
+public import Mathlib.Topology.Algebra.Module.WeakSpace
 
 /-!
 # Weak dual topology
 
-We continue in the setting of `Mathlib/Topology/Algebra/Module/WeakBilin.lean`,
-which defines the weak topology given two vector spaces `E` and `F` over a commutative semiring
-`𝕜` and a bilinear form `B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜`. The weak topology on `E` is the coarsest topology
-such that for all `y : F` every map `fun x => B x y` is continuous.
-
-In this file, we consider two special cases.
-In the case that `F = E →L[𝕜] 𝕜` and `B` being the canonical pairing, we obtain the weak-* topology,
-`WeakDual 𝕜 E := (E →L[𝕜] 𝕜)`. Interchanging the arguments in the bilinear form yields the
-weak topology `WeakSpace 𝕜 E := E`.
+This file defines the weak-* (weak dual) topology on the continuous dual `E →L[𝕜] 𝕜`.
+It is the coarsest topology such that for all `z : E` every evaluation map
+`fun v => v z` is continuous.
 
 ## Main definitions
 
-The main definitions are the types `WeakDual 𝕜 E` and `WeakSpace 𝕜 E`,
-with the respective topology instances on it.
-
-* `WeakDual 𝕜 E` is a type synonym for `Dual 𝕜 E` (when the latter is defined): both are equal to
-  the type `E →L[𝕜] 𝕜` of continuous linear maps from a module `E` over `𝕜` to the ring `𝕜`.
+* `WeakDual 𝕜 E` is a type synonym for `E →L[𝕜] 𝕜` (equal to `Dual 𝕜 E`).
 * The instance `WeakDual.instTopologicalSpace` is the weak-* topology on `WeakDual 𝕜 E`, i.e., the
   coarsest topology making the evaluation maps at all `z : E` continuous.
-* `WeakSpace 𝕜 E` is a type synonym for `E` (when the latter is defined).
-* The instance `WeakSpace.instTopologicalSpace` is the weak topology on `E`, i.e., the
-  coarsest topology such that all `v : dual 𝕜 E` remain continuous.
 
 ## References
 
@@ -132,82 +120,12 @@ end Ring
 
 end WeakDual
 
-/-- The weak topology is the topology coarsest topology on `E` such that all functionals
-`fun x => v x` are continuous. -/
-def WeakSpace (𝕜 E) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
-    [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :=
-  WeakBilin (topDualPairing 𝕜 E).flip
-deriving AddCommMonoid, Module 𝕜, TopologicalSpace, ContinuousAdd
-
 section Semiring
 
 variable [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
 variable [ContinuousConstSMul 𝕜 𝕜]
 variable [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]
 
-namespace WeakSpace
-
-instance instModule' [CommSemiring 𝕝] [Module 𝕝 E] : Module 𝕝 (WeakSpace 𝕜 E) :=
-  WeakBilin.instModule' (topDualPairing 𝕜 E).flip
-
-instance instIsScalarTower [CommSemiring 𝕝] [Module 𝕝 𝕜] [Module 𝕝 E] [IsScalarTower 𝕝 𝕜 E] :
-    IsScalarTower 𝕝 𝕜 (WeakSpace 𝕜 E) :=
-  WeakBilin.instIsScalarTower (topDualPairing 𝕜 E).flip
-
-instance instContinuousSMul [ContinuousSMul 𝕜 𝕜] : ContinuousSMul 𝕜 (WeakSpace 𝕜 E) :=
-  WeakBilin.instContinuousSMul _
-
-variable [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace 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) : WeakSpace 𝕜 E →L[𝕜] WeakSpace 𝕜 F :=
-  { f with
-    cont :=
-      WeakBilin.continuous_of_continuous_eval _ fun l => WeakBilin.eval_continuous _ (l ∘L f) }
-
-theorem map_apply (f : E →L[𝕜] F) (x : E) : WeakSpace.map f x = f x :=
-  rfl
-
-@[simp]
-theorem coe_map (f : E →L[𝕜] F) : (WeakSpace.map f : E → F) = f :=
-  rfl
-
-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 toWeakSpaceCLM : E →L[𝕜] WeakSpace 𝕜 E where
-  __ := toWeakSpace 𝕜 E
-  cont := by
-    apply WeakBilin.continuous_of_continuous_eval
-    exact ContinuousLinearMap.continuous
-
-variable (𝕜 E) in
-@[simp]
-theorem toWeakSpaceCLM_eq_toWeakSpace (x : E) :
-    toWeakSpaceCLM 𝕜 E x = toWeakSpace 𝕜 E x := by rfl
-
-theorem toWeakSpaceCLM_bijective :
-    Function.Bijective (toWeakSpaceCLM 𝕜 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 (toWeakSpaceCLM 𝕜 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 ((toWeakSpaceCLM 𝕜 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) ↔
@@ -215,20 +133,3 @@ theorem tendsto_iff_forall_eval_tendsto_topDualPairing {l : Filter α} {f : α 
   WeakBilin.tendsto_iff_forall_eval_tendsto _ ContinuousLinearMap.coe_injective
 
 end Semiring
-
-section Ring
-
-namespace WeakSpace
-
-variable [CommRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] [ContinuousConstSMul 𝕜 𝕜]
-variable [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E]
-
-instance instAddCommGroup : AddCommGroup (WeakSpace 𝕜 E) :=
-  WeakBilin.instAddCommGroup (topDualPairing 𝕜 E).flip
-
-instance instIsTopologicalAddGroup : IsTopologicalAddGroup (WeakSpace 𝕜 E) :=
-  WeakBilin.instIsTopologicalAddGroup (topDualPairing 𝕜 E).flip
-
-end WeakSpace
-
-end Ring
diff --git a/Mathlib/Topology/Algebra/Module/WeakSpace.lean b/Mathlib/Topology/Algebra/Module/WeakSpace.lean
new file mode 100644
index 00000000000000..164511adb9363f
--- /dev/null
+++ b/Mathlib/Topology/Algebra/Module/WeakSpace.lean
@@ -0,0 +1,137 @@
+/-
+Copyright (c) 2021 Kalle Kytölä. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kalle Kytölä, Moritz Doll
+-/
+module
+
+public import Mathlib.LinearAlgebra.BilinearMap
+public import Mathlib.Topology.Algebra.Module.LinearMap
+public import Mathlib.Topology.Algebra.Module.WeakBilin
+
+/-!
+# Weak topology
+
+This file defines the weak topology on a topological vector space `E`.
+It is the coarsest topology on `E` such that all continuous linear functionals
+`fun x => v x` for `v : E →L[𝕜] 𝕜` remain continuous.
+
+## Main definitions
+
+* `WeakSpace 𝕜 E` is a type synonym for `E`.
+* The instance `WeakSpace.instTopologicalSpace` is the weak topology on `E`, i.e., the
+  coarsest topology such that all `v : E →L[𝕜] 𝕜` remain continuous.
+* `toWeakSpace`: The canonical linear equivalence `E ≃ₗ[𝕜] WeakSpace 𝕜 E`.
+* `toWeakSpaceCLM`: The identity mapping as a continuous linear map `E →L[𝕜] WeakSpace 𝕜 E`.
+
+## References
+
+* [H. H. Schaefer, *Topological Vector Spaces*][schaefer1966]
+
+## Tags
+
+weak topology, duality
+-/
+
+@[expose] public section
+
+noncomputable section
+
+open Filter Topology
+
+variable {α 𝕜 𝕝 E F : Type*}
+
+/-- The weak topology is the topology coarsest topology on `E` such that all functionals
+`fun x => v x` are continuous. -/
+def WeakSpace (𝕜 E) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
+    [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :=
+  WeakBilin (topDualPairing 𝕜 E).flip
+deriving AddCommMonoid, Module 𝕜, TopologicalSpace, ContinuousAdd
+
+section Semiring
+
+variable [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
+variable [ContinuousConstSMul 𝕜 𝕜]
+variable [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]
+
+namespace WeakSpace
+
+instance instModule' [CommSemiring 𝕝] [Module 𝕝 E] : Module 𝕝 (WeakSpace 𝕜 E) :=
+  WeakBilin.instModule' (topDualPairing 𝕜 E).flip
+
+instance instIsScalarTower [CommSemiring 𝕝] [Module 𝕝 𝕜] [Module 𝕝 E] [IsScalarTower 𝕝 𝕜 E] :
+    IsScalarTower 𝕝 𝕜 (WeakSpace 𝕜 E) :=
+  WeakBilin.instIsScalarTower (topDualPairing 𝕜 E).flip
+
+instance instContinuousSMul [ContinuousSMul 𝕜 𝕜] : ContinuousSMul 𝕜 (WeakSpace 𝕜 E) :=
+  WeakBilin.instContinuousSMul _
+
+variable [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace 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) : WeakSpace 𝕜 E →L[𝕜] WeakSpace 𝕜 F :=
+  { f with
+    cont :=
+      WeakBilin.continuous_of_continuous_eval _ fun l => WeakBilin.eval_continuous _ (l ∘L f) }
+
+theorem map_apply (f : E →L[𝕜] F) (x : E) : WeakSpace.map f x = f x :=
+  rfl
+
+@[simp]
+theorem coe_map (f : E →L[𝕜] F) : (WeakSpace.map f : E → F) = f :=
+  rfl
+
+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 toWeakSpaceCLM : E →L[𝕜] WeakSpace 𝕜 E where
+  __ := toWeakSpace 𝕜 E
+  cont := by
+    apply WeakBilin.continuous_of_continuous_eval
+    exact ContinuousLinearMap.continuous
+
+variable (𝕜 E) in
+@[simp]
+theorem toWeakSpaceCLM_eq_toWeakSpace (x : E) :
+    toWeakSpaceCLM 𝕜 E x = toWeakSpace 𝕜 E x := by rfl
+
+theorem toWeakSpaceCLM_bijective :
+    Function.Bijective (toWeakSpaceCLM 𝕜 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 (toWeakSpaceCLM 𝕜 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 ((toWeakSpaceCLM 𝕜 E) '' V : Set (WeakSpace 𝕜 E))) : IsOpen V := by
+  simpa [Set.image_image] using isOpenMap_toWeakSpace_symm _ hV
+
+end Semiring
+
+section Ring
+
+namespace WeakSpace
+
+variable [CommRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] [ContinuousConstSMul 𝕜 𝕜]
+variable [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E]
+
+instance instAddCommGroup : AddCommGroup (WeakSpace 𝕜 E) :=
+  WeakBilin.instAddCommGroup (topDualPairing 𝕜 E).flip
+
+instance instIsTopologicalAddGroup : IsTopologicalAddGroup (WeakSpace 𝕜 E) :=
+  WeakBilin.instIsTopologicalAddGroup (topDualPairing 𝕜 E).flip
+
+end WeakSpace
+
+end Ring