theorem FourierTransformation.fourier_continuousLinearMap {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℂ F] : ∃ (T : SchwartzMap V F →L[ℂ] SchwartzMap V F), ∀ (f : SchwartzMap V F), T f = FourierTransform.fourier f

The Fourier transform restricts to a continuous ℂ-linear self-map of Schwartz space: there exists T : 𝓢(V, F) →L[ℂ] 𝓢(V, F) whose underlying function agrees with 𝓕 on every Schwartz function.