feat: the space of Schwartz maps is T3 (#40931)

Proves that the space of Schwartz functions is T2. The proof is basically a copy-paste of the same proof for `TestFunction`. 

Thanks to @BenKBreen for pointing out this was missing. 

Co-Authored by: Luigi Massacci @luigimassacci-ax

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: luigi-massacci

Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean

@@ -1202,6 +1202,15 @@ theorem toBoundedContinuousFunctionCLM_apply (f : 𝓢(E, F)) (x : E) :
     toBoundedContinuousFunctionCLM 𝕜 E F f x = f x :=
   rfl
 
+theorem toBoundedContinuousFunctionCLM_injective :
+    Function.Injective (toBoundedContinuousFunctionCLM .. : 𝓢(E, F) →L[𝕜] E →ᵇ F) :=
+  fun _ _ h ↦ DFunLike.ext _ _ fun x ↦ DFunLike.congr_fun h x
+
+instance : T3Space 𝓢(E, F) :=
+  suffices T2Space 𝓢(E, F) from inferInstance
+  .of_injective_continuous (toBoundedContinuousFunctionCLM_injective ℝ ..)
+    (ContinuousLinearMap.continuous _)
+
 end BoundedContinuousFunction
 
 section ZeroAtInfty