Separating family of seminorms (source code)

= Separating family of seminorms
{title2=$\bigcap_{p\in\mathcal P}\ker p=\{0\}$}

A family of <seminorms> separates points when every nonzero <vector> $z$ has $p(z)>0$ for some member $p$. Equivalently, its <kernels of seminorms> have intersection $\{0\}$, or any two distinct <vectors> $x,y$ have $p(x-y)>0$ for some $p$. Individual <seminorms> can have large <kernels of seminorms>; the whole family must have no common invisible direction.

The associated <seminorm topology> is <Hausdorff> if and only if the family separates points. Indeed, if $p(x-y)=a>0$, the <neighbourhoods> $\{u:p(u-x)<a/3\}$ and $\{v:p(v-y)<a/3\}$ are disjoint by the <triangle inequality>. Conversely, if every $p$ vanishes on a nonzero $z$, then zero and $z$ belong to exactly the same open <sets> and cannot be separated. This criterion keeps separation distinct from <completeness>: detecting all directions does not guarantee that all <Cauchy sequences> have limits.