For real normed spaces \(E\), \(F\), the uniformity of Mathlib’s canonical Schwartz space \(\mathcal{S}(E,F)\) is countably generated, coming from the \(\mathbb {N}\times \mathbb {N}\)-indexed seminorm family \(p_{k,n}(\varphi ) = \sup _x \| x\| ^k \| D^n\varphi (x)\| \). When \(F\) is complete, \(\mathcal{S}(E,F)\) is a complete space for this uniformity: the analytic heart is that a sequence of \(C^\infty \) functions converging pointwise, with all iterated derivatives converging uniformly, has a \(C^\infty \) limit whose iterated derivatives are those uniform limits. Via Mathlib’s metrization of countably generated uniformities, the Baire and barrelled-space instances follow, all attached to the canonical topology with no re-metrization.

If a family \((\mathcal{F}_i)_{i \in \iota }\) of continuous linear functionals on \(\mathcal{S}(\mathbb {R},\mathbb {R})\) is pointwise bounded (for each \(\varphi \) there is \(C\) with \(|\mathcal{F}_i \varphi | \le C\) for all \(i\)), then there is a single continuous seminorm \(q\) with \(|\mathcal{F}_i \varphi | \le q(\varphi )\) for all \(i\) and \(\varphi \). This is Banach–Steinhaus in dominating-seminorm form, available because \(\mathcal{S}\) is barrelled. As a companion, a countable pointwise supremum \(\varphi \mapsto \sup _i |\mathcal{F}_i \varphi |\) whose seminorm family is bounded above is itself continuous.