continuity
case intro.hg.refine_1.hp.hf
n : ℕ
A✝ a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
σ' : ℝ
this : Continuous (𝓕 ψ.toFun)
⊢ Continuous fun u => ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π))
no goals