mathlib

bcf8d82b - feat(analysis/normed_space/hahn_banach/separation): generalize to (locally convex) topological vector spaces (#16796)

feat(analysis/normed_space/hahn_banach/separation): generalize to (locally convex) topological vector spaces (#16796) Co-authored-by: Moritz Doll <moritz.doll@googlemail.com> Co-authored-by: Moritz Doll <doll@uni-bremen.de> Co-authored-by: mcdoll <moritz.doll@googlemail.com>