specialize this f x
E : Type u_1
F : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : Measure.IsAddHaarMeasure volume
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k : ℕ
f : 𝓢(E, F)
x : E
this :
  ∀ (f : 𝓢(E, F)) (x : E),
    (1 + ‖x‖) ^ k * ‖f x‖ ≤ 2 ^ k * (Finset.sup (Finset.Iic (k, 0)) fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f
⊢ (1 + ‖x‖) ^ k * ‖f x‖ ≤ 2 ^ k * sup_Iic_seminorm 𝕜 k 0 f
E : Type u_1
F : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : Measure.IsAddHaarMeasure volume
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k : ℕ
f : 𝓢(E, F)
x : E
this : (1 + ‖x‖) ^ k * ‖f x‖ ≤ 2 ^ k * (Finset.sup (Finset.Iic (k, 0)) fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f
⊢ (1 + ‖x‖) ^ k * ‖f x‖ ≤ 2 ^ k * sup_Iic_seminorm 𝕜 k 0 f