Commit 2023-06-29 08:26 5e6d9102

feat(Analysis/LocallyConvex/WithSeminorms): characterize continuous seminorms (#5501) This shows that, if the topology of E is defined by some family of seminorms p, then a seminorm q is continuous iff ∃ s : Finset ι, ∃ C : ℝ≥0, C ≠ 0 ∧ q ≤ C • s.sup p. Via Seminorm.continuous_iff_continuous_comp this gives the converse of Seminorm.continuous_from_bounded and hence a characterization of continuous linear maps between such spaces. To do that, we restate all of the "bound of shell" lemmas in terms of seminorms, which needs changing some imports, but I've checked the current state of the port and this should not cause too much trouble since most of the touched files are already ported so we can changes the imports in mathlib4 too. The WithSeminorms file needs a naming/dot notation refactor at some point, because the naming scheme is neither predictable nor convenient to use, but this PR is already large enough.