Weak Dual in Topological Vector Spaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
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.