Continuity and Von Neumann boundedness #
This files proves that for E
and F
two topological vector spaces over ℝ
or ℂ
,
if E
is first countable, then every locally bounded linear map E →ₛₗ[σ] F
is continuous
(this is LinearMap.continuous_of_locally_bounded
).
We keep this file separate from Analysis/LocallyConvex/Bounded
in order not to import
Analysis/NormedSpace/IsROrC
there, because defining the strong topology on the space of
continuous linear maps will require importing Analysis/LocallyConvex/Bounded
in
Analysis/NormedSpace/OperatorNorm
.
References #
- [Bourbaki, Topological Vector Spaces][bourbaki1987]
Construct a continuous linear map from a linear map f : E →ₗ[𝕜] F
and the existence of a
neighborhood of zero that gets mapped into a bounded set in F
.
Instances For
If E
is first countable, then every locally bounded linear map E →ₛₗ[σ] F
is continuous.