no goals
α : Type u_1
x y z : ℝ
l : Filter α
f : α → ℝ
⊢ ((fun x => 1) =O[l] fun x => exp (f x)) ↔ IsBoundedUnder (fun x x_1 => x ≥ x_1) l f
simp only [← exp_zero, isBigO_exp_comp_exp_comp, Pi.sub_def, zero_sub, isBoundedUnder_le_neg]