α : Type u_2
β : Type u_1
inst✝ : NormedField β
l : Filter α
f g : α → β
hf : BoundedAtFilter l f
hg : BoundedAtFilter l g
⊢ (fun x => OfNat.ofNat 1 x * OfNat.ofNat 1 x) =O[l] 1
α : Type u_2
β : Type u_1
inst✝ : NormedField β
l : Filter α
f g : α → β
hf : BoundedAtFilter l f
hg : BoundedAtFilter l g
⊢ BoundedAtFilter l (f * g)
refine' (hf.mul hg).trans _
case h.e'_8.h
α : Type u_2
β : Type u_1
inst✝ : NormedField β
l : Filter α
f g : α → β
hf : BoundedAtFilter l f
hg : BoundedAtFilter l g
x✝ : α
⊢ OfNat.ofNat 1 x✝ = OfNat.ofNat 1 x✝ * OfNat.ofNat 1 x✝
α : Type u_2
β : Type u_1
inst✝ : NormedField β
l : Filter α
f g : α → β
hf : BoundedAtFilter l f
hg : BoundedAtFilter l g
⊢ (fun x => OfNat.ofNat 1 x * OfNat.ofNat 1 x) =O[l] 1
convert Asymptotics.isBigO_refl (E := ℝ) _ l
no goals
case h.e'_8.h
α : Type u_2
β : Type u_1
inst✝ : NormedField β
l : Filter α
f g : α → β
hf : BoundedAtFilter l f
hg : BoundedAtFilter l g
x✝ : α
⊢ OfNat.ofNat 1 x✝ = OfNat.ofNat 1 x✝ * OfNat.ofNat 1 x✝
simp