mathlib

77db6f75 - feat(analysis/locally_convex/with_seminorms): split `continuous_from_bounded` to get an extra continuity criterion (#16710)

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.