Commit 2022-10-01 21:30 77db6f75

feat(analysis/locally_convex/with_seminorms): split continuous_from_bounded to get an extra continuity criterion (#16710) This split should also help with proving that continuous_from_bounded is an iff under some assumptions, because the only remaining fact to prove is that a continuous seminorm is necessarily greater than a constant times the supremum of a finite number of generating seminorms.