no goals
α : Type u_1
x y z : ℝ
l : Filter α
f : α → ℝ
⊢ ((fun x => exp (f x)) =Θ[l] fun x => 1) ↔ IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => abs (f x)
simp only [← exp_zero, isTheta_exp_comp_exp_comp, sub_zero]