Weak Dual in Topological Vector Spaces #
We prove that the weak topology induced by a bilinear form
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜 is locally
convex and we explicit give a neighborhood basis in terms of the family of seminorms
λ x, ∥B x y∥
y : F.
Main definitions #
Main statements #
linear_map.has_basis_weak_bilin: the seminorm balls of
B.to_seminorm_family form a
neighborhood basis of
0 in the weak topology.
linear_map.to_seminorm_family.with_seminorms: the topology of a weak space is induced by the
family of seminorm
weak_bilin.locally_convex_space: a spaced endowed with a weak topology is locally convex.
weak dual, seminorm
Construct a seminorm from a linear form
f : E →ₗ[𝕜] 𝕜 over a normed field
λ x, ∥f x∥
Construct a family of seminorms from a bilinear form.