l : Filter ℂ
hre : Tendsto re l atTop
him : IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun z => Abs.abs z.im
⊢ im =O[l] fun z => z.re ^ 0
l : Filter ℂ
hre : Tendsto re l atTop
him : IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun z => Abs.abs z.im
⊢ im =O[l] fun z => z.re ^ ↑0
norm_cast
no goals
l : Filter ℂ
hre : Tendsto re l atTop
him : IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun z => Abs.abs z.im
⊢ im =O[l] fun z => z.re ^ 0
simpa only [pow_zero] using @IsBoundedUnder.isBigO_const ℂ ℝ ℝ _ _ _ l him 1 one_ne_zero