∀ {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [inst : Norm E] [inst_1 : NormedAddCommGroup F''] {f : α → E}
  {l : Filter α}, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ f) → ∀ {c : F''}, c ≠ 0 → f =O[l] fun _x => c