Topological vector spaces over the real and complex fields

Fix $\mathbb{K}=\mathbb{R}$ or $\mathbb{C}$, with metric $d(s,t)=\mathrm{\mid }s-t\mathrm{\mid }$ from The absolute value makes $\mathbb{R}$ a metric space: $d(x,y)=\mathrm{\mid }x-y\mathrm{\mid }$ is a metric, its open balls are the intervals $(x-r,x+r)$, and it is unbounded or The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane and topology The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement. The topology axioms follow from Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed. Its finite-intersection argument selects radii from finitely many nonempty admissible-radius sets by Every natural-number-indexed list of nonempty sets has a choice function on its family of values, then takes their positive minimum. No AC is assumed.

A topological vector space (TVS) is a $\mathbb{K}$-vector space $X$ (Vector space over a field) with a topology (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison) for which addition $(x,y)\mapsto x+y$ on $X\times X$ and scalar multiplication $(a,x)\mapsto ax$ on $\mathbb{K}\times X$ are jointly continuous (Continuity of a map of topological spaces at a point and globally). Both domains have The product set ${\prod }_{i\in I}{X}_i$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space.

A zero-neighborhood contains an open set containing $0$ (Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open); it need not be open. A Hausdorff TVS additionally has disjoint open neighborhoods for distinct points (Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not). Hausdorffness is a separate hypothesis.

The zero vector space with its unique topology is allowed. A vector space is nonempty because it contains its specified zero. No norm, metric on $X$, local convexity or choice assumption is included.