no goals
α : Type u_1
x y z : ℝ
l : Filter α
f : α → ℝ
⊢ ((fun x => exp (f x)) =O[l] fun x => 1) ↔ IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
simp only [isBigO_one_iff, norm_eq_abs, abs_exp, isBoundedUnder_le_exp_comp]