Commit 2022-10-02 15:17 b2381e5a
View on Github →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.