theorem TemperedDistributions.continuous_of_isBounded_schwartz {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {G : Type u_2} [NormedAddCommGroup G] [NormedSpace ℝ G] (T : SchwartzMap E G →ₗ[ℝ] SchwartzMap E G) (hbound : Seminorm.IsBounded (schwartzSeminormFamily ℝ E G) (schwartzSeminormFamily ℝ E G) T) : Continuous ⇑T

A linear map between Schwartz spaces is continuous if it is bounded with respect to the canonical Schwartz seminorm family. One direction of Melrose's Lemma 7.4.

theorem TemperedDistributions.isBounded_schwartz_of_continuous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {G : Type u_2} [NormedAddCommGroup G] [NormedSpace ℝ G] (T : SchwartzMap E G →L[ℝ] SchwartzMap E G) : Seminorm.IsBounded (schwartzSeminormFamily ℝ E G) (schwartzSeminormFamily ℝ E G) ↑T

A continuous linear map between Schwartz spaces is bounded with respect to the canonical Schwartz seminorm family. Reverse direction of Melrose's Lemma 7.4.

theorem TemperedDistributions.continuous_linearMap_schwartz_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {G : Type u_2} [NormedAddCommGroup G] [NormedSpace ℝ G] (T : SchwartzMap E G →ₗ[ℝ] SchwartzMap E G) : Continuous ⇑T ↔ Seminorm.IsBounded (schwartzSeminormFamily ℝ E G) (schwartzSeminormFamily ℝ E G) T

Melrose's Lemma 7.4: a linear map between Schwartz spaces is continuous iff it is bounded with respect to the canonical Schwartz seminorm family.