mathlib3

ce3997c6 - feat(analysis/locally_convex): Add construction of continuous linear maps (#15922)

feat(analysis/locally_convex): Add construction of continuous linear maps (#15922) This is the first part of the theorem that for a pseudometrizable locally convex space boundedness implies continuity. Co-authored-by: Moritz Doll <doll@uni-bremen.de>