Theorem: isLittleO_const_of_tendsto_atTop (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
α : Type u_1
inst✝ : Preorder α
a : ℝ
f : α → ℝ
hf : Tendsto f atTop atTop
⊢ (fun x => a) =o[atTop] f
Tactic:
simp [tendsto_norm_atTop_atTop.comp hf]
State after:
no goals