WStarAlgebras have Unique Preduals

1. Dual Pairs and Weak Topologies🔗

This chapter collects the locally convex input to the rest of the blueprint. Throughout, \mathbb{K} is \mathbb{R} or \mathbb{C}, and B : E \times F \to \mathbb{K} is a bilinear form, or pairing, between vector spaces E and F. The ultraweak topology on a W^*-algebra M is the case E = M, F = M_*. Most of the results here are destined for mathlib.

Definition1.1
uses 0
Used by 5
Reverse dependency previews
Preview
Lemma 1.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

The weak topology \sigma(E, F) on E is the coarsest topology for which the functionals x \mapsto B(x, y) are continuous for every y \in F. We say that a topology on E is weak for B if it coincides with \sigma(E, F).

Lean code for Definition1.1●2 definitions
  • defdefined in Mathlib/Topology/Algebra/Module/Spaces/WeakBilin.lean
    complete
    def WeakBilin.{u_2, u_4, u_5} {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5}
  [CommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F]
  [Module 𝕜 F] : (E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) → Type u_4
    def WeakBilin.{u_2, u_4, u_5} {𝕜 : Type u_2}
  {E : Type u_4} {F : Type u_5}
  [CommSemiring 𝕜] [AddCommMonoid E]
  [Module 𝕜 E] [AddCommMonoid F]
  [Module 𝕜 F] :
  (E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) → Type u_4
    The space `E` equipped with the weak topology induced by the bilinear form `B`.
  • class(1 method)defined in LeanOA/IsWeak.lean
    complete
    class LinearMap.IsWeak.{u_2, u_3, u_4} {𝕜 : Type u_2} {E : Type u_3}
  {F : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [AddCommMonoid E]
  [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [t : TopologicalSpace E]
  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) : Prop
    class LinearMap.IsWeak.{u_2, u_3, u_4}
  {𝕜 : Type u_2} {E : Type u_3}
  {F : Type u_4} [CommSemiring 𝕜]
  [TopologicalSpace 𝕜] [AddCommMonoid E]
  [Module 𝕜 E] [AddCommMonoid F]
  [Module 𝕜 F] [t : TopologicalSpace E]
  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) : Prop
    Typeclass expressing that the topology on `E` is the weak topology induced
by the bilinear form `B`.

    Methods

    eq_induced : t = TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace
Definition1.2
uses 0
Used by 5
Reverse dependency previews
Preview
Lemma 1.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

A topology on E is compatible with B if every continuous linear functional on E is of the form x \mapsto B(x, y) for exactly one y \in F; that is, y \mapsto B(\cdot, y) is a linear isomorphism of F onto the continuous dual E' of E.

Lean code for Definition1.2●1 definition
  • class(2 methods)defined in LeanOA/Mathlib/Analysis/LocallyConvex/IsCompatibleDual.lean
    complete
    class LinearMap.IsCompatibleDual.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E]
  [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F]
  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) : Prop
    class LinearMap.IsCompatibleDual.{u_1, u_2, u_3}
  {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3}
  [NontriviallyNormedField 𝕜]
  [AddCommGroup E] [Module 𝕜 E]
  [TopologicalSpace E] [AddCommGroup F]
  [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
  Prop
    A linear topology on `E` is compatible with the bilinear form `B` if the
every continuous linear functional on `E` has the form `B.flip f` for exactly one `f : F`.

    Methods

    range_eq_range : B.flip.range = (ContinuousLinearMap.coeLM 𝕜).range
    injective : Function.Injective ⇑B.flip
Lemma1.3
Statement uses 2
Statement dependency previews
Preview
Definition 1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 1.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Every \sigma(E, F)-continuous linear functional on E is of the form B(\cdot, y) for some y \in F. Consequently, if B separates the points of F, then \sigma(E, F) is compatible with B.

Lean code for Lemma1.3●2 declarations
  • theoremdefined in LeanOA/IsWeak.lean
    complete
    theorem LinearMap.IsWeak.eval_surjective.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜]
  [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F]
  [TopologicalSpace E] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [hB : B.IsWeak] :
  Function.Surjective ⇑(LinearMap.IsWeak.eval B)
    theorem LinearMap.IsWeak.eval_surjective.{u_1,
    u_2, u_3}
  {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3}
  [NontriviallyNormedField 𝕜]
  [AddCommGroup E] [Module 𝕜 E]
  [AddCommGroup F] [Module 𝕜 F]
  [TopologicalSpace E]
  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)
  [hB : B.IsWeak] :
  Function.Surjective
    ⇑(LinearMap.IsWeak.eval B)
    The **Weak Representation Theorem**: Every continuous functional on `E` endowed with
the `σ(E, F; B)`-topology is of the form `x ↦ B(x, y)` for some `y : F`.
  • defdefined in LeanOA/IsWeak.lean
    complete
    def LinearMap.IsWeak.rightDualEquiv.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜]
  [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F]
  [TopologicalSpace E] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [hB : B.IsWeak]
  (hr : B.SeparatingRight) : F ≃ₗ[𝕜] StrongDual 𝕜 E
    def LinearMap.IsWeak.rightDualEquiv.{u_1, u_2,
    u_3}
  {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3}
  [NontriviallyNormedField 𝕜]
  [AddCommGroup E] [Module 𝕜 E]
  [AddCommGroup F] [Module 𝕜 F]
  [TopologicalSpace E]
  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [hB : B.IsWeak]
  (hr : B.SeparatingRight) :
  F ≃ₗ[𝕜] StrongDual 𝕜 E
    When `B` is right-separating, `F` is linearly equivalent to the strong dual of `E` with the
weak topology.
Proof for Lemma 1.3
uses 0

If f is \sigma(E, F)-continuous, then |f(x)| \le C \max_i |B(x, y_i)| for some C \ge 0 and finitely many y_1, \ldots, y_n \in F. So f vanishes on the common kernel of the functionals B(\cdot, y_i), and is therefore a linear combination of them, which is B(\cdot, y) for some y in the span of the y_i. Uniqueness of y is exactly the statement that B separates the points of F.

Theorem1.4
uses 0
Used by 3
Reverse dependency previews
Preview
Theorem 1.7
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsmathlib

(Banach-Alaoglu) The closed unit ball of the dual space of a normed vector space is compact in the weak-* topology.

Lean code for Theorem1.4●1 theorem
  • theoremdefined in Mathlib/Analysis/Normed/Module/WeakDual.lean
    complete
    theorem WeakDual.isCompact_closedBall.{u_1, u_3} {𝕜 : Type u_1} {E : Type u_3}
  [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E]
  [NormedSpace 𝕜 E] [ProperSpace 𝕜] (x' : StrongDual 𝕜 E) (r : ℝ) :
  IsCompact (⇑WeakDual.toStrongDual ⁻¹' Metric.closedBall x' r)
    theorem WeakDual.isCompact_closedBall.{u_1, u_3}
  {𝕜 : Type u_1} {E : Type u_3}
  [NontriviallyNormedField 𝕜]
  [SeminormedAddCommGroup E]
  [NormedSpace 𝕜 E] [ProperSpace 𝕜]
  (x' : StrongDual 𝕜 E) (r : ℝ) :
  IsCompact
    (⇑WeakDual.toStrongDual ⁻¹'
      Metric.closedBall x' r)
    The **Banach-Alaoglu theorem**: closed balls of the dual of a normed space `E` are compact in
the weak-star topology.

For s \subseteq E, the polar of s is s^\circ = \{y \in F \mid |B(x, y)| \le 1 \text{ for all } x \in s\}, and the polar of a subset of F is defined symmetrically.

Theorem1.5
Statement uses 3
Statement dependency previews
Preview
Definition 1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Corollary 1.6
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

(Bipolar theorem) Suppose that E carries the weak topology \sigma(E, F), or more generally a locally convex topology compatible with B. Then for every nonempty s \subseteq E, the bipolar s^{\circ\circ} is the closed absolutely convex hull of s.

Lean code for Theorem1.5●2 theorems
  • theoremdefined in LeanOA/Mathlib/Analysis/LocallyConvex/Bipolar.lean
    complete
    theorem LinearMap.flip_polar_polar.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [AddCommGroup F]
  [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [TopologicalSpace E]
  [hB : B.IsWeak] {s : Set E} (hs : s.Nonempty) :
  B.flip.polar (B.polar s) = (closedAbsConvexHull 𝕜) s
    theorem LinearMap.flip_polar_polar.{u_1, u_2, u_3}
  {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3} [RCLike 𝕜]
  [AddCommGroup E] [AddCommGroup F]
  [Module 𝕜 E] [Module 𝕜 F]
  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)
  [TopologicalSpace E] [hB : B.IsWeak]
  {s : Set E} (hs : s.Nonempty) :
  B.flip.polar (B.polar s) =
    (closedAbsConvexHull 𝕜) s
  • theoremdefined in LeanOA/Mathlib/Analysis/LocallyConvex/Bipolar.lean
    complete
    theorem LinearMap.IsCompatibleDual.flip_polar_polar.{u_4, u_5, u_6}
  {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [RCLike 𝕜]
  [AddCommGroup E] [Module 𝕜 E] [Module ℝ E] [IsScalarTower ℝ 𝕜 E]
  [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [LocallyConvexSpace ℝ E] [AddCommGroup F] [Module 𝕜 F]
  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [hB : B.IsCompatibleDual] {s : Set E}
  (h : s.Nonempty) :
  B.flip.polar (B.polar s) = (closedAbsConvexHull 𝕜) s
    theorem LinearMap.IsCompatibleDual.flip_polar_polar.{u_4,
    u_5, u_6}
  {𝕜 : Type u_4} {E : Type u_5}
  {F : Type u_6} [RCLike 𝕜]
  [AddCommGroup E] [Module 𝕜 E]
  [Module ℝ E] [IsScalarTower ℝ 𝕜 E]
  [TopologicalSpace E]
  [IsTopologicalAddGroup E]
  [ContinuousSMul 𝕜 E]
  [LocallyConvexSpace ℝ E]
  [AddCommGroup F] [Module 𝕜 F]
  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)
  [hB : B.IsCompatibleDual] {s : Set E}
  (h : s.Nonempty) :
  B.flip.polar (B.polar s) =
    (closedAbsConvexHull 𝕜) s
Proof for Theorem 1.5
uses 0

The bipolar is closed, absolutely convex, and contains s, so it contains the closed absolutely convex hull K of s. Conversely, if x_0 \notin K, the Hahn–Banach separation theorem yields a continuous linear functional f on E and a real number c > 0 with |f(x)| \le c < \operatorname{Re} f(x_0) for all x \in K. By Lemma 1.3, or by compatibility, f = B(\cdot, y) for some y \in F, so y / c \in s^\circ while |B(x_0, y / c)| > 1, and therefore x_0 \notin s^{\circ\circ}.

Corollary1.6
uses 1used by 1✓L∃∀N

Under the hypotheses of Theorem 1.5, let W \subseteq E be a subspace. Then W^\circ is the annihilator W^\perp = \{y \in F \mid B(x, y) = 0 \text{ for all } x \in W\}, and (W^\perp)^\perp is the closure of W.

Lean code for Corollary1.6●2 theorems
  • theoremdefined in LeanOA/Mathlib/Analysis/LocallyConvex/PolarSubmodule.lean
    complete
    theorem LinearMap.IsWeak.flip_polarSubmodule_polarSubmodule.{u_1, u_2, u_3}
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜]
  [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F]
  [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E]
  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [B.IsWeak] (W : Submodule 𝕜 E) :
  B.flip.polarSubmodule (B.polarSubmodule W) = W.topologicalClosure
    theorem LinearMap.IsWeak.flip_polarSubmodule_polarSubmodule.{u_1,
    u_2, u_3}
  {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3} [RCLike 𝕜]
  [AddCommGroup E] [Module 𝕜 E]
  [AddCommGroup F] [Module 𝕜 F]
  [TopologicalSpace E] [ContinuousAdd E]
  [ContinuousConstSMul 𝕜 E]
  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [B.IsWeak]
  (W : Submodule 𝕜 E) :
  B.flip.polarSubmodule
      (B.polarSubmodule W) =
    W.topologicalClosure
    If `E` carries the weak topology induced by `B`, then the bipolar of a submodule is its
closure.
  • theoremdefined in LeanOA/Mathlib/Analysis/LocallyConvex/PolarSubmodule.lean
    complete
    theorem LinearMap.IsCompatibleDual.flip_polarSubmodule_polarSubmodule.{u_1, u_2,
    u_3}
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜]
  [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F]
  [Module ℝ E] [IsScalarTower ℝ 𝕜 E] [TopologicalSpace E]
  [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [LocallyConvexSpace ℝ E] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [B.IsCompatibleDual]
  (W : Submodule 𝕜 E) :
  B.flip.polarSubmodule (B.polarSubmodule W) = W.topologicalClosure
    theorem LinearMap.IsCompatibleDual.flip_polarSubmodule_polarSubmodule.{u_1,
    u_2, u_3}
  {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3} [RCLike 𝕜]
  [AddCommGroup E] [Module 𝕜 E]
  [AddCommGroup F] [Module 𝕜 F]
  [Module ℝ E] [IsScalarTower ℝ 𝕜 E]
  [TopologicalSpace E]
  [IsTopologicalAddGroup E]
  [ContinuousSMul 𝕜 E]
  [LocallyConvexSpace ℝ E]
  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)
  [B.IsCompatibleDual]
  (W : Submodule 𝕜 E) :
  B.flip.polarSubmodule
      (B.polarSubmodule W) =
    W.topologicalClosure
    If `E` is a locally convex space whose topology is compatible with `B`, then the bipolar of a
submodule is its closure.
Proof for Corollary 1.6
uses 0

Since W is closed under scaling, |B(x, y)| \le 1 for all x \in W forces B(x, y) = 0, so W^\circ = W^\perp, and likewise for subspaces of F. The closed absolutely convex hull of a subspace is its closure, so the claim follows from Theorem 1.5.

Theorem1.7
Statement uses 3
Statement dependency previews
Preview
Definition 1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 4
Reverse dependency previews
Preview
Lemma 2.2.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

(Krein–Smulian) Let E be a Banach space. A convex subset of E^* is weak-* closed if its intersection with every closed ball is weak-* closed. Consequently, if B : X \times E \to \mathbb{K} identifies X with E^* (that is, \sigma(E, X) is compatible with B) and X carries the weak topology \sigma(X, E), then a convex cone in X is closed as soon as its intersection with the closed unit ball is closed, and a linear map from X into a space carrying a weak topology is continuous as soon as it is continuous on the closed unit ball.

Lean code for Theorem1.7●3 theorems
  • theoremdefined in LeanOA/KreinSmulian.lean
    complete
    theorem krein_smulian.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
  (A : Set (WeakDual 𝕜 E))
  (hA :
    ∃ᶠ (r : ℝ) in Filter.atTop,
      IsClosed (A ∩ ⇑WeakDual.toStrongDual ⁻¹' Metric.closedBall 0 r))
  (hA_conv : Convex 𝕜 A) : IsClosed A
    theorem krein_smulian.{u_1, u_2} {𝕜 : Type u_1}
  {E : Type u_2} [RCLike 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [CompleteSpace E]
  (A : Set (WeakDual 𝕜 E))
  (hA :
    ∃ᶠ (r : ℝ) in Filter.atTop,
      IsClosed
        (A ∩
          ⇑WeakDual.toStrongDual ⁻¹'
            Metric.closedBall 0 r))
  (hA_conv : Convex 𝕜 A) : IsClosed A
    The **Krein-Smulian theorem**. If `A : Set (WeakDual 𝕜 E)` is convex and its intersection with
arbitrarily large closed balls is closed, then `A` is itself closed (in the weak⋆ topology).
  • theoremdefined in LeanOA/KreinSmulian.lean
    complete
    theorem krein_smulian_of_submodule.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2}
  [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
  (A : Submodule NNReal (WeakDual 𝕜 E))
  (hA :
    IsClosed (↑A ∩ ⇑WeakDual.toStrongDual ⁻¹' Metric.closedBall 0 1)) :
  IsClosed ↑A
    theorem krein_smulian_of_submodule.{u_1, u_2}
  {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [CompleteSpace E]
  (A : Submodule NNReal (WeakDual 𝕜 E))
  (hA :
    IsClosed
      (↑A ∩
        ⇑WeakDual.toStrongDual ⁻¹'
          Metric.closedBall 0 1)) :
  IsClosed ↑A
    The **Krein-Smulian theorem**. If `A : Submodule 𝕜 (WeakDual 𝕜 E)` and if
the intersection of `A` with the closed unit ball is closed, then `A` is itself
closed (in the weak⋆ topology).
  • theoremdefined in LeanOA/KreinSmulian.lean
    complete
    theorem LinearMap.IsWeak.continuous_of_continuousOn_closedBall.{u_1, u_2, u_3,
    u_4, u_5}
  {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] [CompleteSpace E] {X : Type u_3} [AddCommGroup X]
  [Module 𝕜 X] [TopologicalSpace X] (B : X →ₗ[𝕜] E →ₗ[𝕜] 𝕜) [B.IsWeak]
  [B.flip.IsCompatibleDual] {Y : Type u_4} {G : Type u_5}
  [AddCommGroup Y] [Module 𝕜 Y] [TopologicalSpace Y] [AddCommGroup G]
  [Module 𝕜 G] (C : Y →ₗ[𝕜] G →ₗ[𝕜] 𝕜) [C.IsWeak] (f : X →ₗ[𝕜] Y)
  (hf :
    ContinuousOn (⇑f)
      (⇑(LinearMap.IsCompatibleDual.equiv B.flip) ⁻¹'
        Metric.closedBall 0 1)) :
  Continuous ⇑f
    theorem LinearMap.IsWeak.continuous_of_continuousOn_closedBall.{u_1,
    u_2, u_3, u_4, u_5}
  {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [CompleteSpace E] {X : Type u_3}
  [AddCommGroup X] [Module 𝕜 X]
  [TopologicalSpace X]
  (B : X →ₗ[𝕜] E →ₗ[𝕜] 𝕜) [B.IsWeak]
  [B.flip.IsCompatibleDual] {Y : Type u_4}
  {G : Type u_5} [AddCommGroup Y]
  [Module 𝕜 Y] [TopologicalSpace Y]
  [AddCommGroup G] [Module 𝕜 G]
  (C : Y →ₗ[𝕜] G →ₗ[𝕜] 𝕜) [C.IsWeak]
  (f : X →ₗ[𝕜] Y)
  (hf :
    ContinuousOn (⇑f)
      (⇑(LinearMap.IsCompatibleDual.equiv
            B.flip) ⁻¹'
        Metric.closedBall 0 1)) :
  Continuous ⇑f
    A linear map from a space with the weak topology of a pairing `B` with a Banach space into a
space carrying the weak topology of another pairing `C` is continuous if it is continuous on the
closed unit ball.
Proof for Theorem 1.7
uses 0

The first statement is proved by an inductive construction of a sequence of finite sets in E, tending to zero, whose polars separate a point outside the convex set from the set itself; compactness of the intersections with closed balls (Theorem 1.4) drives each step. For the consequences, X is homeomorphic to E^* with its weak-* topology, and a linear map into a weak topology is continuous if and only if each of its compositions with the defining functionals is; the preimage of a closed set under such a composition, intersected with a closed ball, is closed by hypothesis.