simpa
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
this : ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ 0 (⇑f) x‖ ^ 1 ≤ C * (1 + ‖x‖)⁻¹
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖)⁻¹
no goals