mathlib
mathlib copied to clipboard
Locally convex Hausdorff spaces
We have the definition of locally convex spaces and the characterization of locally convex spaces via seminorms. We have all the ingredients to prove the very useful lemma: Let X be a vector space and P be a family of seminorms. Show that the topology induced by P is Hausdorff if and only if for every non-zero vector x ∈ X there exists a seminorm p ∈ P , such that p(x) ≠ 0.