Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

Locally convex Hausdorff spaces #15565

Open
mcdoll opened this issue Jul 20, 2022 · 0 comments
Open

Locally convex Hausdorff spaces #15565

mcdoll opened this issue Jul 20, 2022 · 0 comments
Labels
feature-request This issue is a feature request, either for mathematics, tactics, or CI good-first-project

Comments

@mcdoll
Copy link
Member

mcdoll commented Jul 20, 2022

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.

@mcdoll mcdoll added feature-request This issue is a feature request, either for mathematics, tactics, or CI good-first-project labels Jul 20, 2022
bors bot pushed a commit that referenced this issue Dec 19, 2022
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 <[email protected]>
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
feature-request This issue is a feature request, either for mathematics, tactics, or CI good-first-project
Projects
None yet
1 participant