mathlib

d2617e08 - feat(analysis/locally_convex): locally convex hausdorff spaces (#17937)

feat(analysis/locally_convex): locally convex hausdorff spaces (#17937) Adds that locally convex spaces whose topology is induced by a family of seminorms are Hausdorff iff the family of seminorms is separating, together with some helper lemmas. Closes issue #15565. Co-authored-by: Lukas Miaskiwskyi <lukas.mias@googlemail.com>