mathlib

b2381e5a - feat(analysis/locally_convex/with_seminorms): boundedness of images (#16674)

feat(analysis/locally_convex/with_seminorms): boundedness of images (#16674) This PR adds two lemmas that are very useful in proving that semilinear maps are locally bounded (and hence continuous). We also add some documentation for these lemmas and remove documentation for the ad-hoc lemmas.