In functional analysis and related areas, a complete topological vector space (TVS) is a topological vector space in which every Cauchy net or Cauchy filter converges to a point of the space. The notion of "points that get progressively closer" is made rigorous by Cauchy nets or Cauchy filters, which generalize Cauchy sequences, while "a point towards which they all get closer" means that such a net or filter converges to that point. Completeness for TVSs is formulated using the theory of uniform spaces to generalize completeness from metric spaces; unlike metric completeness, TVS-completeness does not depend on any specific metric and applies to TVSs that may not be metrizable or Hausdorff. For normed spaces and metrizable TVSs, the usual completeness defined by a particular norm or metric coincides with this notion of TVS-completeness, which is independent of any particular choice of norm or metric. A metrizable topological vector space with a translation-invariant metric is complete as a TVS if and only if it is a complete metric space, which by definition means that every Cauchy sequence converges to some point in the space. Prominent examples of complete TVSs that are also metrizable include all F-spaces and, consequently, all Fréchet spaces, Banach spaces, and Hilbert spaces. Prominent examples of complete TVSs that are typically non-metrizable include strict LF-spaces such as the space of test functions with its canonical LF-topology, the strong dual of any non-normable Fréchet space, and many polar topologies on continuous duals or other topologies on spaces of linear maps. Explicitly, a topological vector space (TVS) is complete if every net, or equivalently every filter, that is Cauchy with respect to the space's canonical uniformity converges to some point. Equivalently, a TVS is complete if its canonical uniformity is a complete uniformity. The canonical uniformity on a TVS is the unique translation-invariant uniformity that induces the given topology. This notion of TVS-completeness depends on vector subtraction and the topology of the TVS and therefore applies to all TVSs, including those whose topologies cannot be defined in terms of metrics or pseudometrics. A first-countable TVS is complete if and only if every Cauchy sequence (or equivalently every elementary Cauchy filter) converges. Every topological vector space, even if it is not metrizable or Hausdorff, has a completion, which by definition is a complete TVS into which it can be TVS-embedded as a dense vector subspace. Moreover, when the TVS is Hausdorff the completion is unique up to TVS-isomorphism. In contrast, non-Hausdorff TVSs have infinitely many non-Hausdorff completions that are TVS-isomorphic to one another.

Definitions. This section summarizes the definition of a complete topological vector space (TVS) in terms of nets and prefilters. Information about convergence of nets and filters can be found in the article on filters in topology.

Every TVS is a commutative topological group under addition, and its canonical uniformity is defined in terms of subtraction (hence addition); scalar multiplication is not involved.

Canonical uniformity. Let X be a TVS. For any subset U of X define the entourage V_U = {(x,y) in X×X : x - y is in U}. The canonical uniformity on X is generated by the entourages V_U as U runs over neighborhoods of 0. If U is symmetric (U = -U) then V_U is symmetric; moreover the composition V_U composed with V_U is contained in V_{U+U}, so the family of such entourages satisfies the usual uniformity axioms. If B is any neighborhood basis at the origin, then {V_U : U in B} is a base of entourages (a prefilter on X×X). Equivalently, if N is the neighborhood filter at the origin, then {V_U : U in N} forms a base of entourages for the canonical uniform structure on X. Explicitly, the canonical uniformity on a topological vector space X is the filter on X × X generated by the prefilter of entourages of the diagonal of the form {(x,y) : x − y ∈ U}, where U ranges over the neighborhoods of the origin 0 in X. The same canonical uniformity results if one uses any neighborhood basis at the origin instead of the full filter of all neighborhoods: if B is any neighborhood basis at 0 in X, then the filter on X × X generated by {{(x,y) : x − y ∈ U} : U ∈ B} equals the canonical uniformity induced by the topology of X. 

The general theory of uniform spaces has definitions of a "Cauchy prefilter" and a "Cauchy net". For the canonical uniformity on a TVS these definitions reduce to the following concrete description. Suppose (x_i)_{i∈I} is a net in X and (y_j)_{j∈J} is a net in X. The product I × J becomes a directed set by declaring (i,j) ≤ (i',j') iff i ≤ i' and j ≤ j'. The product net (x_i, y_j)_{(i,j)∈I×J} is the Cartesian product net. Its image under vector addition is the (I × J)-indexed net x_i + y_j, and its image under vector subtraction is the (I × J)-indexed net x_i − y_j. In particular, the notation x_{i,j} denotes the (I × J)-indexed net and not an I-indexed net.

A net (x_i) in a TVS is called a Cauchy net if for every neighborhood U of 0 in X there exists i_0 ∈ I such that for all i, i' ≥ i_0 we have x_i − x_{i'} ∈ U. It suffices to check this condition for any given neighborhood basis at 0. A Cauchy sequence is a sequence that is also a Cauchy net. Continuity of the vector subtraction map implies that if xα → x and yα → y then xα − yα → x − y, so every convergent net is a Cauchy net. By definition, a space is complete if the converse always holds: a topological vector space is complete if and only if every Cauchy net in the space converges to some point of the space. The same characterization of completeness holds when using filters or prefilters instead of nets. A series is called a Cauchy series (respectively, a convergent series) if the sequence of partial sums is a Cauchy sequence (respectively, a convergent sequence). Every convergent series is a Cauchy series, and in a complete topological vector space every Cauchy series converges. A prefilter on a topological vector space is called a Cauchy prefilter if for every neighborhood U of 0 there exists a member A of the prefilter with A − A ⊂ U; equivalently, the family {A − A : A in the prefilter} forms a prefilter that "converges" to 0.